instRing — Mathlib

English

If R is a ring, then MvPowerSeries σ R carries a ring structure extending the semiring structure.

Русский

Если R — кольцо, то MvPowerSeries σ R имеет кольцевую структуру, расширяющую полусистему.

LaTeX

$$$$ \text{Ring} (\mathrm{MvPowerSeries}(σ,R)) $$$$

Lean4

instance [Ring R] : Ring (MvPowerSeries σ R) :=
  { inferInstanceAs (Semiring (MvPowerSeries σ R)), inferInstanceAs (AddCommGroup (MvPowerSeries σ R)) with }

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