isWeierstrassDivisorAt — Mathlib

English

If g is distinguished at I and I ≠ ⊤, then g is a Weierstrass divisor relative to I.

Русский

Если g IsDistinguishedAt I и I ≠ ⊤, тогда g — дивизор Вайершстраса относительно I.

LaTeX

$$$\\forall {A} [\\text{CommRing } A] (g : A[X]) (I : \\text{Ideal } A) (H : g.IsDistinguishedAt I) (hI : I ≠ ⊤), IsWeierstrassDivisorAt g I$$$

Lean4

theorem _root_.Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt {g : A[X]} {I : Ideal A} (H : g.IsDistinguishedAt I)
    (hI : I ≠ ⊤) : IsWeierstrassDivisorAt g I :=
  by
  have : g.natDegree = _ :=
    congr(ENat.toNat $(H.coe_natDegree_eq_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]) (by simp)))
  simp [IsWeierstrassDivisorAt, ← this, H.monic.leadingCoeff]

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