R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ ↑(aeval (↑ϕ (root f))) f = 0
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ ↑(aeval (↑ϕ (root f))) f = 0
have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ eval₂ (RingHom.comp (↑ϕ) (of f)) (↑ϕ (root f)) f = eval₂ (RingHom.comp (↑ϕ) (of f)) (↑↑ϕ (root f)) f
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ ↑(aeval (↑ϕ (root f))) f = 0
rw [aeval_def, ← h, ← RingHom.map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]
no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ eval₂ (RingHom.comp (↑ϕ) (of f)) (↑ϕ (root f)) f = eval₂ (RingHom.comp (↑ϕ) (of f)) (↑↑ϕ (root f)) f
rfl