C_dvd_iff_isUnit — Mathlib

English

Let p be monic. For any a ∈ R, C(a) divides p in R[X] if and only if a is a unit in R.

Русский

Пусть p моничен. Для любого a ∈ R C(a) делит p в R[X] тогда и только тогда, когда a является единицей в R.

LaTeX

$$$p.Monic \rightarrow (C\ a \mid p) \iff IsUnit\ a$$$

Lean4

theorem C_dvd_iff_isUnit {a : R} : C a ∣ p ↔ IsUnit a
    where
  mp h := isUnit_iff_dvd_one.mpr <| hp.coeff_natDegree ▸ (C_dvd_iff_dvd_coeff _ _).mp h p.natDegree
  mpr ha := (ha.map C).dvd

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