case a.h
α : Type u_1
β : Type ?u.17082
γ : Type ?u.17085
m : Type ?u.17088
n : Type u_2
R : Type ?u.17094
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
α : Type u_1
β : Type ?u.17082
γ : Type ?u.17085
m : Type ?u.17088
n : Type u_2
R : Type ?u.17094
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ M ⊙ 1 = diagonal fun i => M i i
ext i j
no goals
case a.h
α : Type u_1
β : Type ?u.17082
γ : Type ?u.17085
m : Type ?u.17088
n : Type u_2
R : Type ?u.17094
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
by_cases h: i = j <;> simp [h]