Merge branch 'master' into MR-cleanup-lint-style

.github/workflows/bors.yml

@@ -113,6 +113,23 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
+  summarize_declarations:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: summarize_declarations
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
+      - name: print_lost_declarations
+        run: |
+          ## back and forth to settle a "detached head" (maybe?)
+          git checkout -q master
+          git checkout -q -
+          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
+          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
+
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build

.github/workflows/build.yml

@@ -120,6 +120,23 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
+  summarize_declarations:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: summarize_declarations
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
+      - name: print_lost_declarations
+        run: |
+          ## back and forth to settle a "detached head" (maybe?)
+          git checkout -q master
+          git checkout -q -
+          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
+          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
+
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build

.github/workflows/build.yml.in

@@ -99,6 +99,23 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
+  summarize_declarations:
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
+    name: summarize_declarations
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
+      - name: print_lost_declarations
+        run: |
+          ## back and forth to settle a "detached head" (maybe?)
+          git checkout -q master
+          git checkout -q -
+          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
+          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
+
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME

.github/workflows/build_fork.yml

@@ -117,6 +117,23 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
+  summarize_declarations:
+    if: github.repository != 'leanprover-community/mathlib4'
+    name: summarize_declarations
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
+      - name: print_lost_declarations
+        run: |
+          ## back and forth to settle a "detached head" (maybe?)
+          git checkout -q master
+          git checkout -q -
+          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
+          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
+
   build:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Build (fork)

.github/workflows/lean4checker.yml

@@ -62,8 +62,6 @@ jobs:
           # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
           rm -rf .lake/packages/proofwidgets/.lake/build/lib
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
-          # also build MathlibExtras
-          lake build -KCI MathlibExtras
 
       - name: Check environments using lean4checker
         id: lean4checker

Mathlib.lean

@@ -113,6 +113,7 @@ import Mathlib.Algebra.Category.SemigroupCat.Basic
 import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.CharP.CharAndCard
+import Mathlib.Algebra.CharP.Defs
 import Mathlib.Algebra.CharP.ExpChar
 import Mathlib.Algebra.CharP.IntermediateField
 import Mathlib.Algebra.CharP.Invertible
@@ -286,6 +287,7 @@ import Mathlib.Algebra.Homology.ExactSequence
 import Mathlib.Algebra.Homology.Functor
 import Mathlib.Algebra.Homology.HomologicalBicomplex
 import Mathlib.Algebra.Homology.HomologicalComplex
+import Mathlib.Algebra.Homology.HomologicalComplexAbelian
 import Mathlib.Algebra.Homology.HomologicalComplexBiprod
 import Mathlib.Algebra.Homology.HomologicalComplexLimits
 import Mathlib.Algebra.Homology.Homology
@@ -295,6 +297,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
 import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
 import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
+import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
 import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
 import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
 import Mathlib.Algebra.Homology.HomotopyCategory.Shift
@@ -3429,6 +3432,7 @@ import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.Ideal.IdempotentFG
 import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Ideal.LocalRing
+import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.MinimalPrime
 import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.Ideal.Operations
@@ -3642,8 +3646,8 @@ import Mathlib.Tactic.Change
 import Mathlib.Tactic.Check
 import Mathlib.Tactic.Choose
 import Mathlib.Tactic.Clean
-import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
+import Mathlib.Tactic.ClearExclamation
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -12,18 +12,18 @@ import Mathlib.GroupTheory.GroupAction.Pi
 /-!
 # Maps (semi)conjugating a shift to a shift
 
-Denote by \(S^1\) the unit circle `UnitAddCircle`.
-A common way to study a self-map \(f\colon S^1\to S^1\) of degree `1`
-is to lift it to a map \(\tilde f\colon \mathbb R\to \mathbb R\)
-such that \(\tilde f(x + 1) = \tilde f(x)+1\) for all `x`.
+Denote by $S^1$ the unit circle `UnitAddCircle`.
+A common way to study a self-map $f\colon S^1\to S^1$ of degree `1`
+is to lift it to a map $\tilde f\colon \mathbb R\to \mathbb R$
+such that $\tilde f(x + 1) = \tilde f(x)+1$ for all `x`.
 
 In this file we define a structure and a typeclass
 for bundled maps satisfying `f (x + a) = f x + b`.
 
 We use parameters `a` and `b` instead of `1` to accomodate for two use cases:
 
 - maps between circles of different lengths;
-- self-maps \(f\colon S^1\to  S^1\) of degree other than one,
+- self-maps $f\colon S^1\to  S^1$ of degree other than one,
   including orientation-reversing maps.
 -/
 

Mathlib/Algebra/Algebra/Equiv.lean

@@ -663,7 +663,7 @@ end OfLinearEquiv
 
 section OfRingEquiv
 
-/-- Promotes a linear ring_equiv to an AlgEquiv. -/
+/-- Promotes a linear `RingEquiv` to an `AlgEquiv`. -/
 @[simps apply symm_apply toEquiv] -- Porting note: don't want redundant `toEquiv_symm_apply` simps
 def ofRingEquiv {f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = algebraMap R A₂ x) :
     A₁ ≃ₐ[R] A₂ :=

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -59,10 +59,10 @@ structure NonUnitalAlgHom [Monoid R] [Monoid S] (φ : R →* S) (A : Type v) (B
 infixr:25 " →ₙₐ " => NonUnitalAlgHom _
 
 @[inherit_doc]
-notation:25 A " →ₙₐ[" R "] " B => NonUnitalAlgHom (MonoidHom.id R) A B
+notation:25 A " →ₛₙₐ[" φ "] " B => NonUnitalAlgHom φ A B
 
 @[inherit_doc]
-notation:25 A " →ₛₙₐ[" φ "] " B => NonUnitalAlgHom φ A B
+notation:25 A " →ₙₐ[" R "] " B => NonUnitalAlgHom (MonoidHom.id R) A B
 
 attribute [nolint docBlame] NonUnitalAlgHom.toMulHom
 
@@ -116,7 +116,7 @@ instance (priority := 100) {F : Type*} [FunLike F A B] [Module R B] [NonUnitalAl
   { ‹NonUnitalAlgHomClass F R A B› with map_smulₛₗ := map_smulₛₗ }
 
 /-- Turn an element of a type `F` satisfying `NonUnitalAlgSemiHomClass F φ A B` into an actual
-`NonUnitalAlgSemiHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[φ] B`. -/
+`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[φ] B`. -/
 @[coe]
 def toNonUnitalAlgSemiHom {F R S : Type*} [Monoid R] [Monoid S] {φ : R →* S} {A B : Type*}
     [NonUnitalNonAssocSemiring A] [DistribMulAction R A]

Mathlib/Algebra/Algebra/Prod.lean

@@ -15,9 +15,10 @@ The R-algebra structure on `(i : I) → A i` when each `A i` is an R-algebra.
 
 ## Main definitions
 
-* `Pi.algebra`
-* `Pi.evalAlgHom`
-* `Pi.constAlgHom`
+* `Prod.algebra`
+* `AlgHom.fst`
+* `AlgHom.snd`
+* `AlgHom.prod`
 -/
 
 
@@ -98,8 +99,7 @@ theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/
 @[simps]
-def prodEquiv : (A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C)
-    where
+def prodEquiv : (A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C) where
   toFun f := f.1.prod f.2
   invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
   left_inv f := by ext <;> rfl

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -3,9 +3,8 @@ Copyright (c) 2021 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-import Mathlib.Algebra.Star.Pointwise
 import Mathlib.Algebra.Star.Subalgebra
-import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.Tactic.NoncommRing
 
 #align_import algebra.algebra.spectrum from "leanprover-community/mathlib"@"58a272265b5e05f258161260dd2c5d247213cbd3"

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Antoine Chambert-Loir
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
-import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.Maps
 
 #align_import algebra.algebra.subalgebra.basic from "leanprover-community/mathlib"@"b915e9392ecb2a861e1e766f0e1df6ac481188ca"
 

Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

@@ -14,7 +14,7 @@ import Mathlib.GroupTheory.GroupAction.Ring
 This file relates various algebraic structures and provides maps (generally algebra homomorphisms),
 from the unitization of a non-unital subobject into the full structure. The range of this map is
 the unital closure of the non-unital subobject (e.g., `Algebra.adjoin`, `Subring.closure`,
-`Subsemiring.closure` or `StarSubalgebra.adjoin`). When the underlying scalar ring is a field, for
+`Subsemiring.closure` or `StarAlgebra.adjoin`). When the underlying scalar ring is a field, for
 this map to be injective it suffices that the range omits `1`. In this setting we provide suitable
 `AlgEquiv` (or `StarAlgEquiv`) onto the range.
 
@@ -40,7 +40,7 @@ this map to be injective it suffices that the range omits `1`. In this setting w
 * `NonUnitalStarSubalgebra s : Unitization R s →⋆ₐ[R] A`: a version of
   `NonUnitalSubalgebra.unitization` for star algebras.
 * `NonUnitalStarSubalgebra.unitizationStarAlgEquiv s :`
-  `Unitization R s ≃⋆ₐ[R] StarSubalgebra.adjoin R (s : Set A)`:
+  `Unitization R s ≃⋆ₐ[R] StarAlgebra.adjoin R (s : Set A)`:
   a version of `NonUnitalSubalgebra.unitizationAlgEquiv` for star algebras.
 -/
 
@@ -343,7 +343,7 @@ variable {R S A : Type*} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A]
   [StarModule R A] [SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A]
   [StarMemClass S A] (s : S)
 /-- The natural star `R`-algebra homomorphism from the unitization of a non-unital star subalgebra
-to its `StarSubalgebra.adjoin`. -/
+to its `StarAlgebra.adjoin`. -/
 def unitization : Unitization R s →⋆ₐ[R] A :=
   Unitization.starLift <| NonUnitalStarSubalgebraClass.subtype s
 
@@ -369,7 +369,7 @@ theorem unitization_injective (h1 : (1 : A) ∉ s) : Function.Injective (unitiza
   AlgHomClass.unitization_injective s h1 (unitization s) fun _ ↦ by simp
 
 /-- If a `NonUnitalStarSubalgebra` over a field does not contain `1`, then its unitization is
-isomorphic to its `StarSubalgebra.adjoin`. -/
+isomorphic to its `StarAlgebra.adjoin`. -/
 @[simps! apply_coe]
 noncomputable def unitizationStarAlgEquiv (h1 : (1 : A) ∉ s) :
     Unitization R s ≃⋆ₐ[R] StarAlgebra.adjoin R (s : Set A) :=

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -296,8 +296,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
         apply Quotient.sound
         apply leftRel_apply.mpr
         fconstructor
-        exact -x
-        simp only [add_zero, AddMonoidHom.map_neg]
+        · exact -x
+        · simp only [add_zero, AddMonoidHom.map_neg]
   inv :=
     QuotientAddGroup.lift _ (cokernel.π f) <| by
       rintro _ ⟨x, rfl⟩

Mathlib/Algebra/CharP/Algebra.lean

@@ -3,9 +3,9 @@ Copyright (c) 2021 Jon Eugster. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster, Eric Wieser
 -/
-import Mathlib.Algebra.CharP.Basic
-import Mathlib.RingTheory.Localization.FractionRing
+import Mathlib.Algebra.CharP.Defs
 import Mathlib.Algebra.FreeAlgebra
+import Mathlib.RingTheory.Localization.FractionRing
 
 #align_import algebra.char_p.algebra from "leanprover-community/mathlib"@"96782a2d6dcded92116d8ac9ae48efb41d46a27c"