equivUnitsEnd — Mathlib

English

There is a natural MulEquiv between Perm α and Units(End α).

Русский

Существует естественное умножение-эквивалент между Perm α и Units(End α).

LaTeX

$$$\\\\operatorname{Perm}(\\\\alpha) \\\\cong_{\\\\mathrm{Mul}} \\\\mathrm{Units}(\\\\operatorname{End}(\\\\alpha))$$$

Lean4

/-- The permutation of a type is equivalent to the units group of the endomorphisms monoid of this
type. -/
@[simps]
def equivUnitsEnd : Perm α ≃* Units (Function.End α)
    where
  toFun e := ⟨⇑e, ⇑e.symm, e.self_comp_symm, e.symm_comp_self⟩
  invFun u := ⟨(u : Function.End α), (↑u⁻¹ : Function.End α), congr_fun u.inv_val, congr_fun u.val_inv⟩
  map_mul' _ _ := rfl

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