map_monic_eq_zero_iff — Mathlib

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]⟩

Похожие утверждения