permCongrHom — Mathlib

English

For e ∈ α ≃ β, the map permCongrHom(e) is a monoid isomorphism from Perm α to Perm β.

Русский

Для e ∈ α ≃ β отображение permCongrHom(e) является моноидной гомоморфизм-перемонтация между Perm α и Perm β.

LaTeX

$$$$ \mathrm{permCongrHom}: (e: \alpha \cong \beta) \to (Perm\,\alpha \to^* Perm\,\beta). $$$$

Lean4

def _root_.Equiv.permCongrHom (e : α ≃ β) : Perm α ≃* Perm β
    where
  toEquiv := e.permCongr
  map_mul' p q := e.permCongr_mul p q

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