permCongr — Mathlib

English

If α ≃ β, then there is a natural equivalence between the permutation groups Perm α and Perm β. For a given e : α ≃ β, permCongr e e : Perm α ≃ Perm β.

Русский

Если α эквивалентно β, существует естественная эквивалентность между группами перестановок Perm α и Perm β. Для данного e : α ≃ β определено Perm α ≃ Perm β.

LaTeX

$$$\operatorname{Perm}(\alpha')\simeq\operatorname{Perm}(\beta')$$$

Lean4

/-- If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`. -/
def permCongr : Perm α' ≃ Perm β' :=
  equivCongr e e

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