feat: Matrix.abs_det_submatrix_equiv_equiv (#19332)

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Algebra.Ring.Divisibility.Basic
+import Mathlib.Algebra.Ring.Int.Units
 import Mathlib.Data.Nat.Cast.Order.Ring
 
 /-!
@@ -151,6 +152,9 @@ theorem abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a
   simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
     neg_add_rev, neg_neg, add_assoc]
 
+lemma abs_unit_intCast (a : ℤˣ) : |((a : ℤ) : α)| = 1 := by
+  cases Int.units_eq_one_or a <;> simp_all
+
 end LinearOrderedCommRing
 
 section

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

@@ -222,6 +222,17 @@ theorem det_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m R) :
   intro i
   rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]
 
+/-- Permuting rows and columns with two equivalences does not change the absolute value of the
+determinant. -/
+@[simp]
+theorem abs_det_submatrix_equiv_equiv {R : Type*} [LinearOrderedCommRing R]
+    (e₁ e₂ : n ≃ m) (A : Matrix m m R) :
+    |(A.submatrix e₁ e₂).det| = |A.det| := by
+  have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp
+  rw [hee]
+  show |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|
+  rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
+
 /-- Reindexing both indices along the same equivalence preserves the determinant.
 
 For the `simp` version of this lemma, see `det_submatrix_equiv_self`; this one is unsuitable because