case h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - ↑C x}
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - ↑C x}
ext y
no goals
case h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - ↑C x}
simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]