coeff_mem — Mathlib

English

If f is Eisenstein at P, then every coefficient not equal to the leading degree lies in P.

Русский

Если f является Эйзенштейновым относительно P, то каждый коэффициент, кроме ведущего, принадлежит P.

LaTeX

$$$\\forall {f:R[X]}\\; (hf: f.IsEisensteinAt 𝓟) \\to \\forall {n}, n \\neq f.natDegree \\Rightarrow f.coeff n ∈ 𝓟$$$

Lean4

theorem coeff_mem (hf : f.IsEisensteinAt 𝓟) {n : ℕ} (hn : n ≠ f.natDegree) : f.coeff n ∈ 𝓟 :=
  by
  rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂
  · exact hf.mem h₁
  · rw [coeff_eq_zero_of_natDegree_lt h₂]
    exact Ideal.zero_mem _

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