instInvOneClass — Mathlib

English

The formal power series ring k⟦X⟧ admits a natural inverse operation on its units, making the units form a group under multiplication.

Русский

Кольцо формальных степенных рядов k⟦X⟧ обладает естественной операцией обратимости на единицах, образуя группу по умножению.

LaTeX

$$$ (k\langle\langle X\rangle\rangle)^{\times} \text{ is a group under multiplication}. $$$

Lean4

instance : InvOneClass k⟦X⟧ :=
  { inferInstanceAs <| InvOneClass <| MvPowerSeries Unit k with }

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