indexHom — Mathlib

English

The index equivalence of the identity morphism is the identity permutation on ι.

Русский

Индексное эквивалентное отображение тождества является тождественной перестановкой на ι.

LaTeX

$$indexEquiv (P := P) (Q := P) 1 = Equiv.refl ι$$

Lean4

/-- The permutation representation of the endomorphism monoid on the root index set -/
def indexHom (P : RootPairing ι R M N) : End P →* (ι ≃ ι)
    where
  toFun f := Hom.indexEquiv f
  map_one' := by ext; simp
  map_mul' x y := by ext; simp

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