case a.h
l : Type ?u.274619
m : Type ?u.274622
n : Type u_1
o : Type ?u.274628
m' : o → Type ?u.274633
n' : o → Type ?u.274638
R : Type ?u.274641
S : Type ?u.274644
α : Type v
β : Type w
γ : Type ?u.274651
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ ⬝ diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
l : Type ?u.274619
m : Type ?u.274622
n : Type u_1
o : Type ?u.274628
m' : o → Type ?u.274633
n' : o → Type ?u.274638
R : Type ?u.274641
S : Type ?u.274644
α : Type v
β : Type w
γ : Type ?u.274651
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ ⬝ diagonal d₂ = diagonal fun i => d₁ i * d₂ i
ext i j
no goals
case a.h
l : Type ?u.274619
m : Type ?u.274622
n : Type u_1
o : Type ?u.274628
m' : o → Type ?u.274633
n' : o → Type ?u.274638
R : Type ?u.274641
S : Type ?u.274644
α : Type v
β : Type w
γ : Type ?u.274651
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ ⬝ diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j
by_cases i = j <;>
simp [h]