l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ (diagonal fun m => f (↑(algebraMap R (n → α)) r m)) = diagonal (↑(algebraMap R (n → β)) r)
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ map (↑(algebraMap R (Matrix n n α)) r) f = ↑(algebraMap R (Matrix n n β)) r
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ n → f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ (diagonal fun m => f (↑(algebraMap R (n → α)) r m)) = diagonal (↑(algebraMap R (n → β)) r)
simp only [Pi.algebraMap_apply, diagonal_eq_diagonal_iff]
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
i✝ : n
⊢ f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
⊢ n → f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
intro
no goals
l : Type ?u.584026
m : Type ?u.584029
n : Type u_2
o : Type ?u.584035
m' : o → Type ?u.584040
n' : o → Type ?u.584045
R : Type u_1
S : Type ?u.584051
α : Type v
β : Type w
γ : Type ?u.584058
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
i✝ : n
⊢ f (↑(algebraMap R α) r) = ↑(algebraMap R β) r
rw [hf₂]