diagonal — Mathlib

English

The G-set G^n acts on itself diagonally by left multiplication componentwise.

Русский

G^n как G-множество действует на себя по диагонали слева по каждому компоненту.

LaTeX

$$$\text{diagonal}(G,n) : \text{Action}(\text{Type}\,u)\,G$ with $\rho(g)(x_1,\dots,x_n)=(g x_1,\dots,g x_n)$$$

Lean4

/-- The `G`-set `Gⁿ`, acting on itself by left multiplication. -/
abbrev diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) G :=
  Action.ofMulAction G (Fin n → G)

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