case a.h
l : Type ?u.54869
m : Type ?u.54872
n : Type u_2
o : Type ?u.54878
m' : o → Type ?u.54883
n' : o → Type ?u.54888
R : Type u_1
S : Type ?u.54894
α : Type v
β : Type w
γ : Type ?u.54901
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j
l : Type ?u.54869
m : Type ?u.54872
n : Type u_2
o : Type ?u.54878
m' : o → Type ?u.54883
n' : o → Type ?u.54888
R : Type u_1
S : Type ?u.54894
α : Type v
β : Type w
γ : Type ?u.54901
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
⊢ diagonal (r • d) = r • diagonal d
ext i j
no goals
case a.h
l : Type ?u.54869
m : Type ?u.54872
n : Type u_2
o : Type ?u.54878
m' : o → Type ?u.54883
n' : o → Type ?u.54888
R : Type u_1
S : Type ?u.54894
α : Type v
β : Type w
γ : Type ?u.54901
inst✝³ : DecidableEq n
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j
by_cases h : i = j <;>
simp [h]