contentIdeal_generator_dvd_coeff — Mathlib

English

If p.contentIdeal is principal with generator g, then g divides every coefficient of p.

Русский

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

LaTeX

$$$\text{If } p.contentIdeal\ is\ principal\ by\ generator\ g,\ then\ g \mid p.coeff(n)\ for\ all\ n$$$

Lean4

theorem _root_.Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff (h_prin : p.contentIdeal.IsPrincipal) (n : ℕ) :
    h_prin.generator ∣ p.coeff n := by
  have := p.coeff_mem_contentIdeal n
  rw [Submodule.IsPrincipal.mem_iff_eq_smul_generator] at this
  obtain ⟨_, ha⟩ := this
  simp [ha]

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