toPerm — Mathlib

English

The map toPerm sends a DilationEquiv X X to a permutation of X and is a monoid homomorphism.

Русский

Отображение toPerm переводит дилатационные эквивалентности X → X в перестановки множества X и является гомоморфизмом моноида.

LaTeX

$$$\text{toPerm} : (X \simeq^{\mathrm{d}} X) \to^* \operatorname{Equiv.Perm} X$, \\ \\ \text{toFun } e := e.1, \text{map_mul' }\_\_\_ := \mathrm{rfl}, \text{map_one' } := \mathrm{rfl}$$$

Lean4

/-- `DilationEquiv.toEquiv` as a monoid homomorphism. -/
@[simps]
def toPerm : (X ≃ᵈ X) →* Equiv.Perm X where
  toFun e := e.1
  map_mul' _ _ := rfl
  map_one' := rfl

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