factor_dvd_of_not_isUnit — Mathlib

English

If a polynomial f is not a unit, then its factor divides f in the polynomial ring over a field.

Русский

Если многочлен f не является единицей, то factor f делит f в кольце многочленов над полем.

LaTeX

$$$\\neg\\operatorname{IsUnit}(f) \\Rightarrow \\operatorname{factor} f \\mid f$$$

Lean4

theorem factor_dvd_of_not_isUnit {f : K[X]} (hf1 : ¬IsUnit f) : factor f ∣ f :=
  by
  by_cases hf2 : f = 0; · rw [hf2]; exact dvd_zero _
  rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
  exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

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