English
Equivalent to det_comm' in a swapped-inverse context; det(MN) = det(NM) under inverse conditions.
Русский
Эквивалент det_comm' в условиях инверсии; det(MN) = det(NM) при соответствующих предположениях об обратности.
LaTeX
$$det (M * N) = det (N * M)$$
Lean4
/-- If there exists a two-sided inverse `M'` for `M` (indexed differently),
then `det (N * M) = det (M * N)`. -/
theorem det_comm' [DecidableEq m] [DecidableEq n] {M : Matrix n m A} {N : Matrix m n A} {M' : Matrix m n A}
(hMM' : M * M' = 1) (hM'M : M' * M = 1) : det (M * N) = det (N * M) :=
by
nontriviality A
let e := indexEquivOfInv hMM' hM'M
rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm, submatrix_mul_equiv,
Equiv.coe_refl, submatrix_id_id]
