trivial — Mathlib

English

There exists a trivial action of G on V where every g acts as the identity on V.

Русский

Существует тривиальное действие G на V, при котором каждый элемент действует как тождественный отображатель на V.

LaTeX

$$$\text{trivial}(V,G) :\; V \to\mathrm{Action}(V,G)$ with $\rho(g)=1$ for all $g$$$

Lean4

/-- The action defined by sending every group element to the identity. -/
@[simps]
def trivial (X : V) : Action V G :=
  { V := X, ρ := 1 }

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