ι : 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₂)
⊢ vecMul (↑(coords b) x) (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
⊢ vecMul (↑(coords b) x) (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₂))
⊢ vecMul (↑(coords b) x) (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₂)
⊢ vecMul (↑(coords b) x) (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₂))
⊢ vecMul (↑(coords b) x) (toMatrix b ↑b₂)⁻¹ = ↑(coords b₂) x
rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
  Matrix.vecMul_one]