R : Type ?u.22368
inst✝¹¹ : CommRing R
M✝ : Type ?u.22374
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R M✝
M'✝ : Type ?u.22959
inst✝⁸ : AddCommGroup M'✝
inst✝⁷ : Module R M'✝
ι : Type ?u.23501
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M✝
A : Type u_3
inst✝⁴ : CommRing A
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M ⬝ M' = 1
hM'M : M' ⬝ M = 1
✝ : Nontrivial A
⊢ det (M ⬝ N) = det (N ⬝ M)
R : Type ?u.22368
inst✝¹¹ : CommRing R
M✝ : Type ?u.22374
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R M✝
M'✝ : Type ?u.22959
inst✝⁸ : AddCommGroup M'✝
inst✝⁷ : Module R M'✝
ι : Type ?u.23501
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M✝
A : Type u_3
inst✝⁴ : CommRing A
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M ⬝ M' = 1
hM'M : M' ⬝ M = 1
⊢ det (M ⬝ N) = det (N ⬝ M)
nontriviality A
R : Type ?u.22368
inst✝¹¹ : CommRing R
M✝ : Type ?u.22374
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R M✝
M'✝ : Type ?u.22959
inst✝⁸ : AddCommGroup M'✝
inst✝⁷ : Module R M'✝
ι : Type ?u.23501
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M✝
A : Type u_3
inst✝⁴ : CommRing A
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M ⬝ M' = 1
hM'M : M' ⬝ M = 1
✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ det (M ⬝ N) = det (N ⬝ M)
R : Type ?u.22368
inst✝¹¹ : CommRing R
M✝ : Type ?u.22374
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R M✝
M'✝ : Type ?u.22959
inst✝⁸ : AddCommGroup M'✝
inst✝⁷ : Module R M'✝
ι : Type ?u.23501
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M✝
A : Type u_3
inst✝⁴ : CommRing A
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M ⬝ M' = 1
hM'M : M' ⬝ M = 1
✝ : Nontrivial A
⊢ det (M ⬝ N) = det (N ⬝ M)
let e := indexEquivOfInv hMM' hM'M
no goals
R : Type ?u.22368
inst✝¹¹ : CommRing R
M✝ : Type ?u.22374
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R M✝
M'✝ : Type ?u.22959
inst✝⁸ : AddCommGroup M'✝
inst✝⁷ : Module R M'✝
ι : Type ?u.23501
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M✝
A : Type u_3
inst✝⁴ : CommRing A
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M ⬝ M' = 1
hM'M : M' ⬝ M = 1
✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ det (M ⬝ N) = det (N ⬝ M)
rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
  submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]