instIsUniformAddGroup — Mathlib

English

If R is an additive group with uniform structure, then MvPowerSeries σ R inherits a uniform additive group structure.

Русский

Если R — абелева группа с равномерной структурой, то MvPowerSeries σ R наследуют равномерное структурное дополнение по сложению.

LaTeX

$$IsUniformAddGroup (MvPowerSeries σ R)$$

Lean4

/-- The `IsUniformAddGroup` structure on `MvPowerSeries` of a `IsUniformAddGroup` -/
@[scoped instance]
theorem instIsUniformAddGroup [AddGroup R] [IsUniformAddGroup R] : IsUniformAddGroup (MvPowerSeries σ R) :=
  Pi.instIsUniformAddGroup

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