l : Type ?u.519207
m : Type ?u.519210
n : Type u_1
o : Type ?u.519216
m' : o → Type ?u.519221
n' : o → Type ?u.519226
R : Type u_2
S : Type ?u.519232
α : Type v
β : Type w
γ : Type ?u.519239
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
⊢ ↑Algebra.toRingHom r * OfNat.ofNat 1 i j = if i = j then ↑Algebra.toRingHom r else 0
l : Type ?u.519207
m : Type ?u.519210
n : Type u_1
o : Type ?u.519216
m' : o → Type ?u.519221
n' : o → Type ?u.519226
R : Type u_2
S : Type ?u.519232
α : Type v
β : Type w
γ : Type ?u.519239
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
⊢ ↑(algebraMap R (Matrix n n α)) r i j = if i = j then ↑(algebraMap R α) r else 0
dsimp [algebraMap, Algebra.toRingHom, Matrix.scalar]
no goals
l : Type ?u.519207
m : Type ?u.519210
n : Type u_1
o : Type ?u.519216
m' : o → Type ?u.519221
n' : o → Type ?u.519226
R : Type u_2
S : Type ?u.519232
α : Type v
β : Type w
γ : Type ?u.519239
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
i j : n
⊢ ↑Algebra.toRingHom r * OfNat.ofNat 1 i j = if i = j then ↑Algebra.toRingHom r else 0
split_ifs with h <;> simp [h, Matrix.one_apply_ne]