isWeierstrassDivisionAt_zero — Mathlib

English

If g is a power-series over a local ring whose image in the residue field is nonzero, then g is a Weierstrass divisor.

Русский

Если g — степенная серия над локальным кольцом и её образ в остаточном поле не ноль, то g является дивизором Вайершстраса.

LaTeX

$$$\\forall A [\\text{CommRing } A], \\; \\text{IsLocalRing } A \\Rightarrow (g.map (\\text{IsLocalRing.residue } A) \\neq 0) \\Rightarrow g.IsWeierstrassDivisor$$$

Lean4

theorem isWeierstrassDivisionAt_zero : IsWeierstrassDivisionAt 0 g 0 0 I :=
  by
  constructor
  · rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _
  · simp

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