ι : Type ?u.34793
m : Type ?u.34796
n : Type u_2
p : Type ?u.34802
α : Type ?u.34805
R : Type u_1
S : Type ?u.34811
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ (x : n), x ∈ Finset.univ → diag (col a ⬝ row b) x = a x * b x
ι : Type ?u.34793
m : Type ?u.34796
n : Type u_2
p : Type ?u.34802
α : Type ?u.34805
R : Type u_1
S : Type ?u.34811
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ trace (col a ⬝ row b) = a ⬝ᵥ b
apply Finset.sum_congr rfl
no goals
ι : Type ?u.34793
m : Type ?u.34796
n : Type u_2
p : Type ?u.34802
α : Type ?u.34805
R : Type u_1
S : Type ?u.34811
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ (x : n), x ∈ Finset.univ → diag (col a ⬝ row b) x = a x * b x
simp [mul_apply]