instGroup — Mathlib

English

The collection of RelIso r r is a group under composition with identity.

Русский

Набор RelIso r r образует группу по композиции с единицей как тождественным.

LaTeX

$$(\text{RelIso}(r,r), \cdot, \mathrm{id}_r) \text{ is a group}$$

Lean4

instance : Group (r ≃r r) where
  one := .refl r
  mul f₁ f₂ := f₂.trans f₁
  inv := .symm
  mul_assoc _ _ _ := rfl
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  inv_mul_cancel f := ext f.symm_apply_apply

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