R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type ?u.1164003
B' : Type ?u.1164006
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type ?u.1164219
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_1
T : Type u_2
U : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
⊢ ↑ψ (↑(aeval a) p) = eval (↑ψ a) (map (algebraMap T ((fun x => U) a)) (map φ p))
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type ?u.1164003
B' : Type ?u.1164006
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type ?u.1164219
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_1
T : Type u_2
U : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
⊢ ↑ψ (↑(aeval a) p) = ↑(aeval (↑ψ a)) (map φ p)
conv_rhs => rw [aeval_def, ← eval_map]
no goals
R : Type u
S✝ : Type v
T✝ : Type w
A : Type z
A' : Type ?u.1164003
B' : Type ?u.1164006
a✝ b : R
n : ℕ
inst✝¹¹ : CommSemiring A'
inst✝¹⁰ : Semiring B'
inst✝⁹ : CommSemiring R
p✝ q : R[X]
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
B : Type ?u.1164219
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
x : A
S : Type u_1
T : Type u_2
U : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
p : R[X]
a : S
⊢ ↑ψ (↑(aeval a) p) = eval (↑ψ a) (map (algebraMap T ((fun x => U) a)) (map φ p))
rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]