instGroup — Mathlib

English

AddConstEquiv G G a a forms a group under composition, i.e., there is a natural group structure on AddConstEquiv G G a a.

Русский

AddConstEquiv G G a a образует группу относительно композиции; существует естественная группа на AddConstEquiv G G a a.

LaTeX

$$$ \text{AddConstEquiv } G G a a \text{ is a group under composition} $$$

Lean4

instance instGroup : Group (G ≃+c[a, a] G) :=
  toEquiv_injective.group _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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