indexEquiv_mul — Mathlib

English

The action on the root index set ι factors through a permutation representation of the endomorphism monoid End P on ι.

Русский

Действие на множестве индексов корней ι факторизуется через перестановочное представление над моной End P.

LaTeX

$$indexHom : End P →* (ι ≃ ι)$$

Lean4

@[simp]
theorem indexEquiv_mul (P : RootPairing ι R M N) (x y : Hom P P) : indexEquiv (x * y) = indexEquiv x ∘ indexEquiv y :=
  rfl

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