instBaseModule — Mathlib

English

The Hahn series construction yields a semiring when the coefficient ring is a semiring.

Русский

Конструкция Ханна-рядов даёт полукольцо, когда коэффициентный набор образует полукольцо.

LaTeX

$$$\text{HahnSeries}(\Gamma, R) \text{ is a Semiring given appropriate structure on } R$$$

Lean4

instance instBaseModule [Semiring R] [Module R V] : Module R (HahnModule Γ' R V) :=
  inferInstanceAs <| Module R (HahnSeries Γ' V)

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