instGroup — Mathlib

English

If γ is a group with a topological structure, then α →ₘ[μ] γ forms a group under the germ-based constructions (multiplication, inversion, etc.).

Русский

Если γ — группа с топологической структурой, то α →ₘ[μ] γ образует группу по конструкциям на зернах (умножение, инверсия и т.д.).

LaTeX

$$instGroup : Group (α →ₘ[μ] γ)$$

Lean4

@[to_additive existing]
instance instGroup [Group γ] [IsTopologicalGroup γ] : Group (α →ₘ[μ] γ) :=
  toGerm_injective.group _ one_toGerm mul_toGerm inv_toGerm div_toGerm pow_toGerm zpow_toGerm

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