trivial_def — Mathlib

English

For the trivial G-representation on V, the action ρ g is always the identity map on V, for every g ∈ G.

Русский

Для тривиального представления G на V действие ρ g равно единичному отображению на V для каждого g ∈ G.

LaTeX

$$$\text{trivial } k G V.\rho g = \mathrm{id}$$$

Lean4

theorem trivial_def {V : Type u} [AddCommGroup V] [Module k V] (g : G) : (trivial k G V).ρ g = LinearMap.id :=
  rfl

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