leftRegular — Mathlib

English

For any n, the diagonal G-action on k[G^n] is the natural representation obtained by left multiplication in G acting componentwise on G^n.

Русский

Для любого n диагональное действие G на k[G^n] получается естественным представлением, где G действует по компонентам на G^n слева.

LaTeX

$$$\\text{diagonal}(n) = \\text{ofMulAction}(k,G, \\; (\\text{Fin}(n) \\to G))$$$

Lean4

/-- The natural `k`-linear `G`-representation on `k[G]` induced by left multiplication in `G`. -/
noncomputable abbrev leftRegular :=
  ofMulAction k G G

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