instRing — Mathlib

English

If R is a ring, HahnSeries Γ R inherits a ring structure, i.e., HahnSeries Γ R is a ring under the inherited addition and convolution-like multiplication.

Русский

Если R кольцо, то HahnSeries Γ R наследует кольцевую структуру.

LaTeX

$$$[Ring R] \\Rightarrow Ring(\\mathrm{HahnSeries}(\\Gamma,R))$$$

Lean4

instance [Ring R] : Ring (HahnSeries Γ R) :=
  { inferInstanceAs (Semiring (HahnSeries Γ R)), inferInstanceAs (AddCommGroupWithOne (HahnSeries Γ R)) with }

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