ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (toMatrix b ↑b₂)
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
have hu := b.isUnit_toMatrix b₂
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (toMatrix b ↑b₂))
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (toMatrix b ↑b₂)
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
rw [Matrix.isUnit_iff_isUnit_det] at hu
no goals
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (toMatrix b ↑b₂))
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]