Sync upstream mathlib4 (2026-07-31, +8 commits)

Counterexamples/TopologistsSineCurve.lean

@@ -111,7 +111,7 @@ is a continuous image of the positive real line). -/
 theorem isConnected_T : IsConnected T := by
   rw [← closure_S]
   refine (isConnected_Ioi.image _ <| continuousOn_id.prodMk ?_).closure
-  exact continuous_sin.comp_continuousOn <| continuousOn_inv₀.mono fun _ hx ↦ hx.ne'
+  fun_prop (discharger := grind)
 
 /-!
 ## `T` is not path-connected

Mathlib.lean

@@ -5135,6 +5135,8 @@ public import Mathlib.LinearAlgebra.Matrix.Diagonal
 public import Mathlib.LinearAlgebra.Matrix.DotProduct
 public import Mathlib.LinearAlgebra.Matrix.Dual
 public import Mathlib.LinearAlgebra.Matrix.DualNumber
+public import Mathlib.LinearAlgebra.Matrix.Echelon.Basic
+public import Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
 public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 public import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -259,7 +259,7 @@ attribute [instance] AddCommGrpCat.str CommGrpCat.str
 initialize_simps_projections AddCommGrpCat (carrier → coe, -str)
 initialize_simps_projections CommGrpCat (carrier → coe, -str)
 
-/-- `Ab` is an abbreviation for `AddCommGroup`, for the sake of mathematicians' sanity. -/
+/-- `Ab` is an abbreviation for `AddCommGrpCat`, for the sake of mathematicians' sanity. -/
 abbrev Ab := AddCommGrpCat
 
 namespace CommGrpCat
@@ -471,7 +471,7 @@ end CommGrpCat
 
 namespace AddCommGrpCat
 
--- Note that because `ℤ : Type 0`, this forces `G : AddCommGroup.{0}`,
+-- Note that because `ℤ : Type 0`, this forces `G : AddCommGrpCat.{0}`,
 -- so we write this explicitly to be clear.
 -- TODO generalize this, requiring a `ULiftInstances.lean` file
 /-- Any element of an abelian group gives a unique morphism from `ℤ` sending
@@ -504,7 +504,7 @@ def MulEquiv.toGrpIso {X Y : GrpCat} (e : X ≃* Y) : X ≅ Y where
   hom := GrpCat.ofHom e.toMonoidHom
   inv := GrpCat.ofHom e.symm.toMonoidHom
 
-/-- Build an isomorphism in the category `AddGroup` from an `AddEquiv` between `AddGroup`s. -/
+/-- Build an isomorphism in the category `AddGrpCat` from an `AddEquiv` between `AddGroup`s. -/
 add_decl_doc AddEquiv.toAddGrpIso
 
 /-- Build an isomorphism in the category `CommGrpCat` from a `MulEquiv`
@@ -525,15 +525,15 @@ namespace CategoryTheory.Iso
 def groupIsoToMulEquiv {X Y : GrpCat} (i : X ≅ Y) : X ≃* Y :=
   MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp)
 
-/-- Build an `addEquiv` from an isomorphism in the category `AddGroup` -/
+/-- Build an `addEquiv` from an isomorphism in the category `AddGrpCat` -/
 add_decl_doc addGroupIsoToAddEquiv
 
-/-- Build a `MulEquiv` from an isomorphism in the category `CommGroup`. -/
+/-- Build a `MulEquiv` from an isomorphism in the category `CommGrpCat`. -/
 @[to_additive (attr := simps!)]
 def commGroupIsoToMulEquiv {X Y : CommGrpCat} (i : X ≅ Y) : X ≃* Y :=
   MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp)
 
-/-- Build an `AddEquiv` from an isomorphism in the category `AddCommGroup`. -/
+/-- Build an `AddEquiv` from an isomorphism in the category `AddCommGrpCat`. -/
 add_decl_doc addCommGroupIsoToAddEquiv
 
 end CategoryTheory.Iso

Mathlib/Algebra/Group/Submonoid/Support.lean

@@ -54,8 +54,8 @@ theorem mem_mulSupport {x} : x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M :=
 @[to_additive (attr := simp)]
 theorem mulSupport_toSubmonoid : M.mulSupport.toSubmonoid = M ⊓ M⁻¹ := rfl
 
-@[to_additive]
-/- The support of a submonoid is the largest subgroup it contains. -/
+/-- The support of a submonoid is the largest subgroup it contains. -/
+@[to_additive /-- The support of a submonoid is the largest subgroup it contains. -/]
 theorem _root_.Subgroup.gc_toSubmonoid_mulSupport :
     GaloisConnection (α := Subgroup G) Subgroup.toSubmonoid mulSupport :=
   fun _ _ ↦ ⟨fun _ _ ↦ by aesop, fun h _ hx ↦ (h hx).1⟩

Mathlib/Algebra/GroupWithZero/Range.lean

@@ -176,7 +176,8 @@ noncomputable section GroupWithZero
 
 variable [GroupWithZero A] [GroupWithZero B] {f : A →*₀ B}
 
-/- When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide.-/
+/--
+When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide. -/
 lemma valueMonoid_eq_valueGroup : (valueMonoid f) = (valueGroup f).toSubmonoid := by
   rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm]
   apply Submonoid.closure_eq_of_le

Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean

@@ -113,6 +113,33 @@ lemma prod_Ico_mul_eq_prod_Ico_add_one (hab : a ≤ b) (f : α → M) :
 
 end LocallyFiniteOrder
 
+section LocallyFiniteOrderBot
+variable [LocallyFiniteOrderBot α]
+
+@[to_additive (dont_translate := α)]
+lemma prod_Iio_add_one_comm [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α]
+    (a : α) (f : α → M) : ∏ i < a + 1, f i = f a * (∏ i < a, f i) := by
+  simp [Iio_add_one_eq_Iic, ← Iio_insert, Finset.prod_insert]
+
+@[to_additive (dont_translate := α) (attr := simp)]
+lemma prod_Iio_add_one [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α]
+    (a : α) (f : α → M) : ∏ i < a + 1, f i = (∏ i < a, f i) * f a := by
+  simp_rw [prod_Iio_add_one_comm, mul_comm]
+
+@[to_additive (dont_translate := α)]
+lemma prod_Iic_add_one_comm [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α]
+    (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = f (a + 1) * (∏ i ≤ a, f i) := by
+  simp only [← Iio_insert, mem_Iio, lt_self_iff_false, not_false_eq_true, prod_insert,
+    prod_Iio_add_one_comm]
+
+@[to_additive (dont_translate := α) (attr := simp)]
+lemma prod_Iic_add_one [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α]
+    (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1) := by
+  simp_rw [prod_Iic_add_one_comm, mul_comm]
+
+end LocallyFiniteOrderBot
+
+section LocallyFiniteOrderTopBot
 variable [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α]
 
 @[to_additive]
@@ -123,6 +150,8 @@ lemma prod_prod_Ioi_mul_eq_prod_prod_off_diag (f : α → α → M) :
   rw [prod_sigma', prod_sigma']
   refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp
 
+end LocallyFiniteOrderTopBot
+
 end LinearOrder
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/Analysis/Convex/Contractible.lean

@@ -28,7 +28,7 @@ protected theorem StarConvex.contractibleSpace (h : StarConvex ℝ x s) (hne : s
     (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩,
       ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩
   · exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)
-  · exact Continuous.subtype_mk (by fun_prop) _
+  · fun_prop
 
 /-- A non-empty convex set is a contractible space. -/
 protected theorem Convex.contractibleSpace (hs : Convex ℝ s) (hne : s.Nonempty) :

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

@@ -1387,7 +1387,7 @@ theorem denseRange_toLpCLM [FiniteDimensional ℝ E] [BorelSpace E] {p : ℝ≥0
   refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
   obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε
   use (hg₁.toSchwartzMap hg₂).toLp p μ
-  have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᶠ[ae μ] (f : E → F) - g := by
+  have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᵐ[μ] (f : E → F) - g := by
     filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]
     simp
   simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and,

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -364,14 +364,18 @@ theorem gramSchmidtOrthonormalBasis_inv_triangular' {i j : ι} (hij : i < j) :
 /-- Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the
 size of the index set is the dimension of `E`, the matrix of coefficients of `f` with respect to the
 orthonormal basis `gramSchmidtOrthonormalBasis` constructed from `f` is upper-triangular. -/
-theorem gramSchmidtOrthonormalBasis_inv_blockTriangular :
-    ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id := fun _ _ =>
+theorem gramSchmidtOrthonormalBasis_inv_isUpperTriangular :
+    ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).IsUpperTriangular := fun _ _ =>
   gramSchmidtOrthonormalBasis_inv_triangular' h f
 
+@[deprecated (since := "2026-07-30")]
+alias gramSchmidtOrthonormalBasis_inv_blockTriangular :=
+  gramSchmidtOrthonormalBasis_inv_isUpperTriangular
+
 theorem gramSchmidtOrthonormalBasis_det [DecidableEq ι] :
     (gramSchmidtOrthonormalBasis h f).toBasis.det f =
       ∏ i, ⟪gramSchmidtOrthonormalBasis h f i, f i⟫ := by
-  convert! Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
+  convert! Matrix.det_of_isUpperTriangular (gramSchmidtOrthonormalBasis_inv_isUpperTriangular h f)
   exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm
 
 end OrthonormalBasis

Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

@@ -239,7 +239,7 @@ lemma hasSum_weierstrassPExcept (l₀ : ℂ) (z : ℂ) :
       (℘[L - l₀] z) :=
   (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSum
 
-/- `weierstrassPExcept l₀` is differentiable on non-lattice points and `l₀`. -/
+/-- `weierstrassPExcept l₀` is differentiable on non-lattice points and `l₀`. -/
 lemma differentiableOn_weierstrassPExcept (l₀ : ℂ) :
     DifferentiableOn ℂ ℘[L - l₀] (L.lattice \ {l₀})ᶜ := by
   refine (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn

Mathlib/CategoryTheory/Adjunction/Mates.lean

@@ -132,7 +132,7 @@ theorem mateEquiv_counit_symm (α : TwoSquare R₁ H G R₂) (d : D) :
   exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)
 
 set_option backward.defeqAttrib.useBackward true in
-/- A component of a transposed version of the mates correspondence. -/
+/-- A component of a transposed version of the mates correspondence. -/
 theorem unit_mateEquiv (α : TwoSquare G L₁ L₂ H) (c : C) :
     G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ =
       adj₂.unit.app _ ≫ R₂.map (α.app _) := by

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -330,7 +330,7 @@ lemma epi_of_nonempty_of_isConnected {X A : C} [IsConnected A] [h : Nonempty (F.
 lemma surjective_on_fiber_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : Function.Surjective (F.map f) :=
   surjective_of_epi (FintypeCat.incl.map (F.map f))
 
-/- A morphism from an object with non-empty fiber to a connected object is surjective on fibers. -/
+/-- A morphism from an object with non-empty fiber to a connected object is surjective on fibers. -/
 lemma surjective_of_nonempty_fiber_of_isConnected {X A : C} [Nonempty (F.obj X)]
     [IsConnected A] (f : X ⟶ A) :
     Function.Surjective (F.map f) := by

Mathlib/Condensed/Discrete/LocallyConstant.lean

@@ -190,9 +190,7 @@ noncomputable def componentHom (a : Fiber (f.comap g.hom.hom)) :
       simp only [Fiber.mk, Set.mem_preimage, Set.mem_singleton_iff]
       convert! map_eq_image _ _ x
       exact map_preimage_eq_image_map _ _ a⟩
-    continuous_toFun := by
-      -- term mode gives "unknown free variable" error.
-      exact Continuous.subtype_mk (by fun_prop) _ }
+    continuous_toFun := by fun_prop }
 
 lemma incl_comap {S T : (CompHausLike P)ᵒᵖ}
     (f : LocallyConstant S.unop (Y.obj (op (CompHausLike.of P PUnit.{u + 1}))))

Mathlib/Condensed/Light/Sequence.lean

@@ -290,7 +290,7 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] :
     rwa [← LightProfinite.epi_iff_surjective]
   · simp [π', pullback.condition]
   · exact ⟨ConcreteCategory.ofHom ⟨(sectionOfFibreIncl π' σ' hσ'),
-      (.subtype_mk (.subtype_mk (by fun_prop) _) _)⟩, rfl⟩
+      (.subtype_mk (by fun_prop) _)⟩, rfl⟩
   · rw [LightProfinite.epi_iff_surjective]
     exact coverToFun_surjective _ _ hσ hσ'
 

Mathlib/LinearAlgebra/Determinant.lean

@@ -365,17 +365,13 @@ theorem det_eq_zero_iff_ker_ne_bot [IsDomain R] [Free R M] [Module.Finite R M] {
     rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]
     refine ⟨fun i => b.repr v i, by simpa, by simpa [toMatrix_mulVec_repr]⟩
 
-/--
-If the determinant of a map vanishes, then the map is not onto.
-TODO: This should only require `[IsDomain R] [Free R M]`, which we get if we generalize
-`Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean`, which includes
-`LinearMap.ker_eq_bot_iff_range_eq_top`.
--/
-theorem range_lt_top_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M}
+/-- If the determinant of a map vanishes, then the map is not onto. -/
+theorem range_lt_top_of_det_eq_zero [IsDomain R] [Free R M] {f : M →ₗ[R] M}
     (hf : f.det = 0) : range f < ⊤ := by
-  have : Module.Finite 𝕜 M := by simp [finite_of_det_ne_one (f := f), hf]
-  rw [lt_top_iff_ne_top, ne_eq, ← ker_eq_bot_iff_range_eq_top, ← ne_eq, ← bot_lt_iff_ne_bot]
-  exact bot_lt_ker_of_det_eq_zero hf
+  rw [lt_top_iff_ne_top]
+  intro h
+  obtain ⟨g, hg⟩ := f.exists_rightInverse_of_surjective h
+  simpa [hf] using congr_arg LinearMap.det hg
 
 /-- When the function is over the base ring, the determinant is the evaluation at `1`. -/
 @[simp] lemma det_ring (f : R →ₗ[R] R) : f.det = f 1 := by

Mathlib/LinearAlgebra/Matrix/Block.lean

@@ -25,7 +25,7 @@ matrices built out of blocks.
 
 * `Matrix.det_of_blockTriangular`: the determinant of a block triangular matrix
   is equal to the product of the determinants of all the blocks
-* `Matrix.det_of_upperTriangular` and `Matrix.det_of_lowerTriangular`: the determinant of
+* `Matrix.det_of_isUpperTriangular` and `Matrix.det_of_isLowerTriangular`: the determinant of
   a triangular matrix is the product of the entries along the diagonal
 
 ## Tags
@@ -61,6 +61,14 @@ variable [Zero R]
 def BlockTriangular (M : Matrix m m R) (b : m → α) : Prop :=
   ∀ ⦃i j⦄, b j < b i → M i j = 0
 
+/-- `M` is upper triangular: entries below the diagonal vanish. -/
+abbrev IsUpperTriangular [LT m] (M : Matrix m m R) : Prop :=
+  M.BlockTriangular id
+
+/-- `M` is lower triangular: entries above the diagonal vanish. -/
+abbrev IsLowerTriangular [LT m] (M : Matrix m m R) : Prop :=
+  M.BlockTriangular toDual
+
 @[simp]
 protected theorem BlockTriangular.submatrix {f : n → m} (h : M.BlockTriangular b) :
     (M.submatrix f f).BlockTriangular (b ∘ f) := fun _ _ hij => h hij
@@ -85,6 +93,11 @@ protected theorem blockTriangular_transpose_iff {b : m → αᵒᵈ} :
 @[simp]
 theorem blockTriangular_zero : BlockTriangular (0 : Matrix m m R) b := fun _ _ _ => rfl
 
+instance decidableBlockTriangular [DecidableEq R] [Fintype m] [DecidableLT α] :
+    Decidable (M.BlockTriangular b) :=
+  decidable_of_iff (∀ ij : m × m, b ij.2 < b ij.1 → M ij.1 ij.2 = 0)
+    ⟨fun h i j hij => h (i, j) hij, fun h _ hij => h hij⟩
+
 end Zero
 
 protected theorem BlockTriangular.neg [NegZeroClass R] {M : Matrix m m R}
@@ -321,15 +334,19 @@ theorem BlockTriangular.det_fintype [DecidableEq α] [Fintype α] [LinearOrder 
   have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
   exact det_isEmpty
 
-theorem det_of_upperTriangular [LinearOrder m] (h : M.BlockTriangular id) :
+theorem det_of_isUpperTriangular [LinearOrder m] (h : M.IsUpperTriangular) :
     M.det = ∏ i : m, M i i := by
   have : DecidableEq R := Classical.decEq _
   simp_rw [h.det, image_id, det_toSquareBlock_id]
 
-theorem det_of_lowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.BlockTriangular toDual) :
+@[deprecated (since := "2026-07-30")] alias det_of_upperTriangular := det_of_isUpperTriangular
+
+theorem det_of_isLowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.IsLowerTriangular) :
     M.det = ∏ i : m, M i i := by
   rw [← det_transpose]
-  exact det_of_upperTriangular h.transpose
+  exact det_of_isUpperTriangular h.transpose
+
+@[deprecated (since := "2026-07-30")] alias det_of_lowerTriangular := det_of_isLowerTriangular
 
 open Polynomial
 
@@ -342,7 +359,7 @@ theorem matrixOfPolynomials_blockTriangular {R} [Semiring R] {n : ℕ} (p : Fin
 theorem det_matrixOfPolynomials {n : ℕ} (p : Fin n → R[X])
     (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
     (Matrix.of (fun (i j : Fin n) => (p j).coeff i)).det = 1 := by
-  rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
+  rw [Matrix.det_of_isUpperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦
       Nat.le_of_eq (h_deg i)))]
   convert! prod_const_one with x _
   rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]

Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

@@ -196,9 +196,12 @@ lemma BlockTriangular.charpoly {α : Type*} {b : n → α} [LinearOrder α] (h :
     M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly := by
   simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock]
 
-lemma charpoly_of_upperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.BlockTriangular id) :
+lemma charpoly_of_isUpperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.IsUpperTriangular) :
     M.charpoly = ∏ i : n, (X - C (M i i)) := by
-  simp [charpoly, det_of_upperTriangular h.charmatrix]
+  simp [charpoly, det_of_isUpperTriangular h.charmatrix]
+
+@[deprecated (since := "2026-07-30")]
+alias charpoly_of_upperTriangular := charpoly_of_isUpperTriangular
 
 -- This proof follows http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf
 /-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a matrix,

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

@@ -670,7 +670,7 @@ theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Mat
 set_option backward.isDefEq.respectTransparency false in
 /-- The determinant of a 2×2 block matrix with the lower-left block equal to zero is the product of
 the determinants of the diagonal blocks. For the generalization to any number of blocks, see
-`Matrix.det_of_upperTriangular`. -/
+`Matrix.det_of_isUpperTriangular`. -/
 @[simp]
 theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) :
     (Matrix.fromBlocks A B 0 D).det = A.det * D.det := by
@@ -721,7 +721,7 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat
 
 /-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of
 the determinants of the diagonal blocks. For the generalization to any number of blocks, see
-`Matrix.det_of_lowerTriangular`. -/
+`Matrix.det_of_isLowerTriangular`. -/
 @[simp]
 theorem det_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R) :
     (Matrix.fromBlocks A 0 C D).det = A.det * D.det := by