case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ x✝ ∈ LinearMap.ker (RingHom.toSemilinearMap (mapRingHom f)) ↔ x✝ ∈ map C (RingHom.ker f)
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
⊢ LinearMap.ker (RingHom.toSemilinearMap (mapRingHom f)) = map C (RingHom.ker f)
ext
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ Polynomial.map f x✝ = 0 ↔ x✝ ∈ map C (RingHom.ker f)
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ x✝ ∈ LinearMap.ker (RingHom.toSemilinearMap (mapRingHom f)) ↔ x✝ ∈ map C (RingHom.ker f)
simp only [LinearMap.mem_ker, RingHom.toSemilinearMap_apply, coe_mapRingHom]
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ (∀ (n : ℕ), coeff (Polynomial.map f x✝) n = coeff 0 n) ↔ ∀ (n : ℕ), coeff x✝ n ∈ RingHom.ker f
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ Polynomial.map f x✝ = 0 ↔ x✝ ∈ map C (RingHom.ker f)
rw [mem_map_C_iff, Polynomial.ext_iff]
no goals
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ (∀ (n : ℕ), coeff (Polynomial.map f x✝) n = coeff 0 n) ↔ ∀ (n : ℕ), coeff x✝ n ∈ RingHom.ker f
simp_rw [RingHom.mem_ker f, coeff_map, coeff_zero]