English
If p is monic, then p.map f = 0 if and only if for all x ∈ R we have f x = 0.
Русский
Если p монічен, то p.map f = 0 тогда и только тогда, когда для всех x ∈ R выполняется f x = 0.
LaTeX
$$p.Monic → p.map f = 0 ↔ ∀ x, f x = 0$$
Lean4
theorem map_monic_eq_zero_iff (hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
⟨fun hfp x =>
calc
f x = f x * f p.leadingCoeff := by simp only [mul_one, hp.leadingCoeff, f.map_one]
_ = f x * (p.map f).coeff p.natDegree := (congr_arg _ (coeff_map _ _).symm)
_ = 0 := by simp only [hfp, mul_zero, coeff_zero],
fun h => ext fun n => by simp only [h, coeff_map, coeff_zero]⟩