permGroup — Mathlib

English

The set of all permutations on α forms a group under composition.

Русский

Множество всех перестановок на α образует группу под операцией композиции.

LaTeX

$$$\\\\operatorname{Group}(\\\\operatorname{Perm}(\\\\alpha))$$$

Lean4

instance permGroup : Group (Perm α)
    where
  mul_assoc _ _ _ := (trans_assoc _ _ _).symm
  one_mul := trans_refl
  mul_one := refl_trans
  inv_mul_cancel := self_trans_symm
  npow n f := f ^ n
  npow_succ _ _ := coe_fn_injective <| Function.iterate_succ _ _
  zpow := zpowRec fun n f ↦ f ^ n
  zpow_succ' _ _ := coe_fn_injective <| Function.iterate_succ _ _

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