isUnit_shift — Mathlib

English

Let A be a commutative ring and g ∈ A[[X]] have a Weierstrass divisor at I. If n is the order of g modulo I, then the power series Q(X) = ∑_{i≥0} coeff_{i+n}(g) X^i is a unit in A[[X]].

Русский

Пусть A — коммутативное кольцо, g ∈ A[[X]] имеет в отношении I-делитель Вейерштрасса. Обозначим n = ord_I(g). Тогда ряд Q(X) = ∑_{i≥0} coeff_{i+n}(g) X^i является единицей в A[[X]].

LaTeX

$$$ n = (g.map (Ideal.Quotient.mk I)).order.toNat, \\\\quad Q(X) = \\sum_{i \\ge 0} \\operatorname{coeff}_{i+n}(g) X^{i}, \\\\quad Q(X) \\in A[[X]]^{\\times}. $$$

Lean4

theorem isUnit_shift : IsUnit <| mk fun i ↦ coeff (i + (g.map (Ideal.Quotient.mk I)).order.toNat) g := by
  simpa [isUnit_iff_constantCoeff]

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