instIsUniformAddGroup — Mathlib

English

C⋆ᵐᵒᵈ(A,E) is an IsUniformAddGroup, obtained by comap from addEquiv.

Русский

C⋆ᵐᵒᵈ(A,E) образует равномерную группу сложения, полученную через отображение-подстановку addEquiv.

LaTeX

$$$ \text{IsUniformAddGroup}(C⋆ᵐᵒᵈ(A,E))$$$

Lean4

instance [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] : IsUniformAddGroup C⋆ᵐᵒᵈ(A, E) :=
  IsUniformAddGroup.comap (addEquiv A E)

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