From 4e55520c24737b7a6e76b7f63ac61031cc0c489d Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 15:02:01 +0800 Subject: [PATCH] chore(LinearAlgebra/Matrix/Block): remove an erw --- Mathlib/LinearAlgebra/Matrix/Block.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean index b723063aa7e338..acb3aa256054fa 100644 --- a/Mathlib/LinearAlgebra/Matrix/Block.lean +++ b/Mathlib/LinearAlgebra/Matrix/Block.lean @@ -263,8 +263,7 @@ protected theorem BlockTriangular.det [DecidableEq α] [LinearOrder α] (hM : Bl let he : { a // b' a = l } ≃ { a // b a = l } := haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl) Equiv.subtypeSubtypeEquivSubtype @hc - simp only [toSquareBlock_def] - erw [← Matrix.det_reindex_self he.symm fun i j : { a // b a = l } => M ↑i ↑j] + rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm] rfl · intro i hi j hj apply hM