instAddMonoidWithOne — Mathlib

English

The ring of multivariate power series has an additive monoid with one structure, with natCast given by n ↦ monomial 0 n.

Русский

У кольца многомерных формальных степенных рядов есть структура аддитивного моноида с единицей; нат_cast задаётся через n ↦ monomial 0 n.

LaTeX

$$$$ ext{natCast}(n) = \operatorname{monomial}(0 : σ \to_0 \mathbb{N}, n). $$$$

Lean4

instance : AddMonoidWithOne (MvPowerSeries σ R) :=
  {
    show AddMonoid (MvPowerSeries σ R) by
      infer_instance with
    natCast := fun n => monomial 0 n
    natCast_zero := by simp [Nat.cast]
    natCast_succ := by simp [Nat.cast, monomial_zero_one]
    one := 1 }

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