case H
R : Type u_1
inst✝⁸ : CommRing R
M✝ : Type ?u.2737751
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M' : Type ?u.2738336
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_2
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M✝
A : Type ?u.2739356
inst✝¹ : CommRing A
inst✝ : Module A M✝
M : ι → ι → R
⊢ ↑(Basis.det (basisFun R ι)) M = ↑detRowAlternating M
R : Type u_1
inst✝⁸ : CommRing R
M : Type ?u.2737751
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2738336
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_2
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2739356
inst✝¹ : CommRing A
inst✝ : Module A M
⊢ Basis.det (basisFun R ι) = detRowAlternating
ext M
no goals
case H
R : Type u_1
inst✝⁸ : CommRing R
M✝ : Type ?u.2737751
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M' : Type ?u.2738336
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_2
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M✝
A : Type ?u.2739356
inst✝¹ : CommRing A
inst✝ : Module A M✝
M : ι → ι → R
⊢ ↑(Basis.det (basisFun R ι)) M = ↑detRowAlternating M
rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose]