leadingCoeff_notMem — Mathlib

English

If f is a monic polynomial and P is a proper (not top) ideal of a commutative ring R, then the leading coefficient of f is not in P.

Русский

Если f моничен и P — это правильный идеал (не полное) в кольце R, то ведущий коэффициент f не лежит в P.

LaTeX

$$$\\forall {R} [\\mathrm{CommRing}R] {\\mathcal P} : f.Monic \\to \\mathcal P \\neq \\top \\to f.leadingCoeff \\notin \\mathcal P$$$

Lean4

theorem _root_.Polynomial.Monic.leadingCoeff_notMem (hf : f.Monic) (h : 𝓟 ≠ ⊤) : f.leadingCoeff ∉ 𝓟 :=
  hf.leadingCoeff.symm ▸ (Ideal.ne_top_iff_one _).1 h

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