case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type ?u.67411
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (toMatrix b ↑b₂ ⬝ toMatrix b₂ ↑b) l m = OfNat.ofNat 1 l m
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type ?u.67411
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ toMatrix b ↑b₂ ⬝ toMatrix b₂ ↑b = 1
ext (l m)
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type ?u.67411
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ vecMul (↑(coords b) (↑b₂ l)) (toMatrix b₂ ↑b) m = OfNat.ofNat 1 l m
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type ?u.67411
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (toMatrix b ↑b₂ ⬝ toMatrix b₂ ↑b) l m = OfNat.ofNat 1 l m
change (b₂.toMatrix b).vecMul (b.coords (b₂ l)) m = _
no goals
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type ?u.67411
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ vecMul (↑(coords b) (↑b₂ l)) (toMatrix b₂ ↑b) m = OfNat.ofNat 1 l m
rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]