fix

Author: vihdzp

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 78f34ded6a5f5aa11ea5b7c3120fe5d8422db1da
+    default: aafe3df227b81f681afa3978f9eab0e2bbcd0582
   path:
     description: Checkout destination path.
     required: false

.github/workflows/build_template.yml

@@ -733,17 +733,36 @@ jobs:
         run: |
           lake exe graph
 
+      - name: Checkout local actions
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ github.workflow_sha }}
+          fetch-depth: 1
+          sparse-checkout: .github/actions
+          path: workflow-actions
+
+      - name: Get mathlib-ci
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
+
+      - name: dump declarations and transitive-import counts
+        run: |
+          lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
+            --out decls.txt --imports-out imports.json Mathlib
+
       - name: upload the import graph
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         with:
           name: import-graph
-          path: import_graph.dot
-          ## the default is 90, but we build often, so unless there's a reason
-          ## to care about old copies in the future, just say 7 days for now
-          retention-days: 7
+          path: |
+            import_graph.dot
+            decls.txt
+            imports.json
+          ## Master pushes: 90 days, so later PRs forked from these commits
+          ## can consume the dumps from the artifact. Other branches: 7 days.
+          retention-days: ${{ github.ref == 'refs/heads/master' && '90' || '7' }}
 
       - name: clean up the import graph file
-        run: rm import_graph.dot
+        run: rm -f import_graph.dot decls.txt imports.json
 
       - name: check all scripts build successfully
         run: |

Mathlib.lean

@@ -1326,6 +1326,7 @@ public import Mathlib.AlgebraicGeometry.AffineSpace
 public import Mathlib.AlgebraicGeometry.AffineTransitionLimit
 public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
 public import Mathlib.AlgebraicGeometry.Artinian
+public import Mathlib.AlgebraicGeometry.Birational.Dominant
 public import Mathlib.AlgebraicGeometry.Birational.RationalMap
 public import Mathlib.AlgebraicGeometry.ColimitsOver
 public import Mathlib.AlgebraicGeometry.Cover.Directed
@@ -4862,6 +4863,7 @@ public import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
 public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
 public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
 public import Mathlib.LinearAlgebra.AffineSpace.Basis
 public import Mathlib.LinearAlgebra.AffineSpace.Centroid
 public import Mathlib.LinearAlgebra.AffineSpace.Ceva
@@ -5111,6 +5113,7 @@ public import Mathlib.LinearAlgebra.Projection
 public import Mathlib.LinearAlgebra.Projectivization.Action
 public import Mathlib.LinearAlgebra.Projectivization.Basic
 public import Mathlib.LinearAlgebra.Projectivization.Cardinality
+public import Mathlib.LinearAlgebra.Projectivization.Collinear
 public import Mathlib.LinearAlgebra.Projectivization.Constructions
 public import Mathlib.LinearAlgebra.Projectivization.Independence
 public import Mathlib.LinearAlgebra.Projectivization.Subspace
@@ -5346,6 +5349,7 @@ public import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 public import Mathlib.MeasureTheory.Function.LpSeminorm.Trim
 public import Mathlib.MeasureTheory.Function.LpSpace.Basic
 public import Mathlib.MeasureTheory.Function.LpSpace.Complete
+public import Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
 public import Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
 public import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 public import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
@@ -5522,6 +5526,7 @@ public import Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
 public import Mathlib.MeasureTheory.Measure.Real
 public import Mathlib.MeasureTheory.Measure.Regular
 public import Mathlib.MeasureTheory.Measure.RegularityCompacts
+public import Mathlib.MeasureTheory.Measure.ResolventTransform
 public import Mathlib.MeasureTheory.Measure.Restrict
 public import Mathlib.MeasureTheory.Measure.SeparableMeasure
 public import Mathlib.MeasureTheory.Measure.Stieltjes
@@ -5690,6 +5695,7 @@ public import Mathlib.NumberTheory.LSeries.ZMod
 public import Mathlib.NumberTheory.LSeries.ZetaZeros
 public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 public import Mathlib.NumberTheory.LegendreSymbol.Basic
+public import Mathlib.NumberTheory.LegendreSymbol.Complex
 public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
 public import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
 public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
@@ -7236,6 +7242,7 @@ public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.OverlappingInstances
 public import Mathlib.Tactic.Linter.PPRoundtrip
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
@@ -7982,6 +7989,7 @@ public import Mathlib.Topology.Sheaves.Abelian
 public import Mathlib.Topology.Sheaves.AddCommGrpCat
 public import Mathlib.Topology.Sheaves.Alexandrov
 public import Mathlib.Topology.Sheaves.CommRingCat
+public import Mathlib.Topology.Sheaves.EtaleSpace
 public import Mathlib.Topology.Sheaves.Flasque
 public import Mathlib.Topology.Sheaves.Forget
 public import Mathlib.Topology.Sheaves.Functors

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -101,6 +101,15 @@ local notation "↑ₐ" => algebraMap R A
 theorem mem_iff {r : R} {a : A} : r ∈ σ a ↔ ¬IsUnit (↑ₐ r - a) :=
   Iff.rfl
 
+@[simp]
+theorem resolvent_zero_of_mem_spectrum {r : R} {a : A} (hr : r ∈ σ a) :
+    resolvent a r = 0 := Ring.inverse_non_unit _ (mem_iff.mp hr)
+
+theorem mem_spectrum_iff_resolvent_zero [Nontrivial A] {r : R} {a : A} :
+    r ∈ σ a ↔ resolvent a r = 0 := by
+  refine ⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩
+  simpa [mem_iff, Ring.not_isUnit_iff_inverse_eq_zero]
+
 theorem notMem_iff {r : R} {a : A} : r ∉ σ a ↔ IsUnit (↑ₐ r - a) := by
   simp [mem_iff]
 

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -517,6 +517,34 @@ theorem subset_adjoin : s ⊆ adjoin R s :=
 @[aesop 80% (rule_sets := [SetLike])]
 theorem mem_adjoin_of_mem {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s := subset_adjoin hx
 
+/-
+The following set-up allows one to write `xₖ : R[x₁, ..., xₙ]` instead of
+`(⟨xₖ, "membership proof"⟩ : R[x₁, ..., xₙ])`.
+
+The idea is to recurse through the list of `x₁, ..., xₙ` until we find the appropriate `xₖ`.
+By design, it only triggers if the set is of the form `insert x₁ (insert x₂ (...(s)))` or
+`{x₁, ..., xₙ}`.
+-/
+
+variable {α : Type*}
+
+/-- Supporting class for coercions `xₖ : R[x₁, ..., xₙ]`. -/
+class CoeAdjoinAux (x : α) (s : Set α) : Prop where mem : x ∈ s
+
+scoped instance (x : α) : CoeAdjoinAux x {x} := ⟨Set.mem_singleton x⟩
+
+scoped instance (x : α) (s : Set α) : CoeAdjoinAux x (insert x s) := ⟨Set.mem_insert x s⟩
+
+scoped instance (x y : α) (s : Set α) [CoeAdjoinAux x s] : CoeAdjoinAux x (insert y s) :=
+  ⟨Set.mem_insert_of_mem y CoeAdjoinAux.mem⟩
+
+/-- Enables notation `xₖ : R[x₁, ..., xₙ]` instead of
+`(⟨xₖ, "membership proof"⟩ : R[x₁, ..., xₙ])`. -/
+scoped instance {A B : Type*} [CommSemiring A] [Semiring B] [Algebra A B]
+    (s : Set B) (x : B) [CoeAdjoinAux x s] :
+    CoeDep B x (adjoin A s) where
+  coe := ⟨x, mem_adjoin_of_mem CoeAdjoinAux.mem⟩
+
 theorem adjoin_le {S : Subalgebra R A} (H : s ⊆ S) : adjoin R s ≤ S :=
   Algebra.gc.l_le H
 

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -153,6 +153,7 @@ lemma prod_filter_not_mul_prod_filter (s : Finset ι) (p : ι → Prop) [Decidab
     (∏ x ∈ s with ¬p x, f x) * ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x := by
   rw [mul_comm, prod_filter_mul_prod_filter_not]
 
+set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 theorem prod_filter_xor (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
     (∏ x ∈ s with (Xor (p x) (q x)), f x) =

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -376,6 +376,7 @@ protected lemma nontrivial {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
   exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)
 
+set_option linter.overlappingInstances false in
 omit [IsFiltered J] in
 instance {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     [HasColimit F] [∀ i, Nontrivial (F.obj i)] : Nontrivial ↑(Limits.colimit F) :=

Mathlib/Algebra/Colimit/DirectLimit.lean

@@ -833,8 +833,8 @@ end NonUnitalStarRing
 namespace Algebra
 
 variable [CommSemiring R]
-variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
-variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
+variable [∀ i, Semiring (G i)] [∀ i, Algebra R (G i)]
+variable [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 variable [Nonempty ι]
 
 variable (G f) in

Mathlib/Algebra/Group/Action/Defs.lean

@@ -614,8 +614,8 @@ end CompatibleScalar
 /-- Typeclass for multiplicative actions on multiplicative structures.
 
 The key axiom here is `smul_mul : g • (x * y) = (g • x) * (g • y)`.
-If `G` is a group (with group law multiplication) and `Γ` is its automorphism
-group then there is a natural instance of `MulDistribMulAction Γ G`.
+If `G` is a multiplicative group with automorphism group `Γ`, then there is a natural instance of
+`MulDistribMulAction Γ G`.
 
 The axiom is also satisfied by a Galois group $Gal(L/K)$ acting on the field `L`,
 but here you can use the even stronger class `MulSemiringAction`, which captures
@@ -627,11 +627,27 @@ class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction
   /-- Distributivity of `•` across `*` -/
   smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
 
+/-- Typeclass for additive actions on additive structures.
+
+The key axiom here is `vadd_add : g +ᵥ (x + y) = (g +ᵥ x) + (g +ᵥ y)`.
+If `G` is an additive group with additive automorphism group `Γ`, then there is a natural instance
+of `AddDistribAddAction Γ G`. -/
+@[ext]
+class AddDistribAddAction (M N : Type*) [AddMonoid M] [AddMonoid N] extends AddAction M N where
+  /-- Acting on `0` by a scalar gives `0` -/
+  vadd_zero : ∀ r : M, r +ᵥ (0 : N) = 0
+  /-- Distributivity of `+ᵥ` across `+` -/
+  vadd_add : ∀ (r : M) (x y : N), r +ᵥ (x + y) = (r +ᵥ x) + (r +ᵥ y)
+
 export MulDistribMulAction (smul_one)
+export AddDistribAddAction (vadd_zero)
+
+attribute [to_additive existing] MulDistribMulAction
 
 section MulDistribMulAction
 variable [Monoid M] [Monoid N] [MulDistribMulAction M N]
 
+@[to_additive]
 lemma smul_mul' (a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
   MulDistribMulAction.smul_mul ..
 

Mathlib/Algebra/Group/Action/End.lean

@@ -108,6 +108,7 @@ namespace MulAut
 variable [Monoid M]
 
 /-- The tautological action by `MulAut M` on `M`. -/
+@[to_additive /-- The tautological action by `AddAut M` on `M`. -/]
 instance applyMulAction : MulAction (MulAut M) M where
   smul := (· <| ·)
   one_smul _ := rfl
@@ -116,16 +117,15 @@ instance applyMulAction : MulAction (MulAut M) M where
 /-- The tautological action by `MulAut M` on `M`.
 
 This generalizes `Function.End.applyMulAction`. -/
+@[to_additive /-- The tautological action by `AddAut M` on `M`. -/]
 instance applyMulDistribMulAction : MulDistribMulAction (MulAut M) M where
-  smul := (· <| ·)
-  one_smul _ := rfl
-  mul_smul _ _ _ := rfl
   smul_one := map_one
   smul_mul := map_mul
 
-@[simp] protected lemma smul_def (f : MulAut M) (a : M) : f • a = f a := rfl
+@[to_additive (attr := simp)] protected lemma smul_def (f : MulAut M) (a : M) : f • a = f a := rfl
 
 /-- `MulAut.applyDistribMulAction` is faithful. -/
+@[to_additive /-- `AddAut.applyAddDistribAddAction` is faithful. -/]
 instance apply_faithfulSMul : FaithfulSMul (MulAut M) M where eq_of_smul_eq_smul := MulEquiv.ext
 
 end MulAut
@@ -135,16 +135,8 @@ end MulAut
 namespace AddAut
 variable [AddMonoid M]
 
-/-- The tautological action by `AddAut M` on `M`. -/
-instance applyMulAction : MulAction (AddAut M) M where
-  smul := (· <| ·)
-  one_smul _ := rfl
-  mul_smul _ _ _ := rfl
-
-@[simp] protected lemma smul_def (f : AddAut M) (a : M) : f • a = f a := rfl
-
-/-- `AddAut.applyDistribMulAction` is faithful. -/
-instance apply_faithfulSMul : FaithfulSMul (AddAut M) M where eq_of_smul_eq_smul := AddEquiv.ext
+@[deprecated (since := "2026-05-26")] alias smul_def := AddAut.vadd_def
+@[deprecated (since := "2026-05-26")] alias apply_faithfulSMul := apply_faithfulVAdd
 
 end AddAut