of_map_ne_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `g` is a power series over a local ring such that
its image in the residue field is not zero, then `g` can be used as a Weierstrass divisor. -/
theorem of_map_ne_zero [IsLocalRing A] (hg : g.map (IsLocalRing.residue A) ≠ 0) : g.IsWeierstrassDivisor :=
  by
  rw [IsWeierstrassDivisor, IsWeierstrassDivisorAt, ← IsLocalRing.notMem_maximalIdeal]
  have h := coeff_order hg
  contrapose! h
  rwa [coeff_map, IsLocalRing.residue_eq_zero_iff]

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