case a.h
l : Type ?u.315980
m : Type u_1
n : Type u_2
o : Type ?u.315989
m' : o → Type ?u.315994
n' : o → Type ?u.315999
R : Type ?u.316002
S : Type ?u.316005
α : Type v
β : Type w
γ : Type ?u.316012
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
x✝ : n
⊢ (1 ⬝ M) i✝ x✝ = M i✝ x✝
l : Type ?u.315980
m : Type u_1
n : Type u_2
o : Type ?u.315989
m' : o → Type ?u.315994
n' : o → Type ?u.315999
R : Type ?u.316002
S : Type ?u.316005
α : Type v
β : Type w
γ : Type ?u.316012
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 ⬝ M = M
ext
no goals
case a.h
l : Type ?u.315980
m : Type u_1
n : Type u_2
o : Type ?u.315989
m' : o → Type ?u.315994
n' : o → Type ?u.315999
R : Type ?u.316002
S : Type ?u.316005
α : Type v
β : Type w
γ : Type ?u.316012
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
x✝ : n
⊢ (1 ⬝ M) i✝ x✝ = M i✝ x✝
rw [← diagonal_one, diagonal_mul, one_mul]