tensorUnit_ρ — Mathlib

English

For every g ∈ G, the action morphism ρ_g on the tensor unit is the identity on the tensor unit of V.

Русский

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

LaTeX

$$$\rho(g) = \mathrm{id}_{\boldsymbol{1}_V}$ for all g ∈ G$$

Lean4

@[simp]
theorem tensorUnit_ρ {g : G} : @DFunLike.coe (G →* End (𝟙_ V)) _ _ _ (𝟙_ (Action V G)).ρ g = 𝟙 (𝟙_ V) :=
  rfl

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