contentIdeal_generator_dvd — Mathlib

English

If p.contentIdeal is principal with generator g, then the constant polynomial C(g) divides p.

Русский

Если contentIdeal(p) порождено генератором g, то константный полином C(g) делит p.

LaTeX

$$C\;h\_prin.generator \mid p$$

Lean4

theorem _root_.Submodule.IsPrincipal.contentIdeal_generator_dvd (h_prin : p.contentIdeal.IsPrincipal) :
    C h_prin.generator ∣ p := by
  rw [C_dvd_iff_dvd_coeff]
  exact fun i ↦ h_prin.contentIdeal_generator_dvd_coeff i

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