diagonalOneIsoLeftRegular — Mathlib

English

There is an isomorphism of G-sets between the diagonal action on Fin 1 → G and the left regular action on G.

Русский

Существует изоморфизм G-множест между диагональным действием на Fin 1 → G и левым регулярным действием на G.

LaTeX

$$$\text{diagonal}(G,1) \cong \text{leftRegular}(G)$$$

Lean4

/-- We have `Fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication. -/
def diagonalOneIsoLeftRegular (G : Type*) [Monoid G] : diagonal G 1 ≅ leftRegular G :=
  Action.mkIso (Equiv.funUnique _ _).toIso fun _ => rfl

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