trivial_apply

Mathlib.RepresentationTheory.Basic

URI: https://scilib.ai/kg/mathlib#Representation.trivial_apply

English

For the trivial representation ρ, the action on any v ∈ V by any g ∈ G is given by ρ(g)(v) = v.

Русский

Для тривиального представления ρ действие на любой элемент v ∈ V позицией g ∈ G задаётся как ρ(g)(v) = v.

LaTeX

$$$\forall g \in G, \forall v \in V:\ ρ(g)(v) = v$$$

Lean4

@[simp]
theorem trivial_apply (g : G) (v : V) : trivial k G V g v = v :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru