isTrivial_def

Mathlib.RepresentationTheory.Basic

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

English

If a representation ρ is IsTrivial, then ρ(g) = id_V for all g ∈ G.

Русский

Если представление ρ является IsTrivial, то для любого g ∈ G выполняется ρ(g) = id_V.

LaTeX

$$IsTrivial ρ ⇒ ∀ g, ρ(g) = LinearMap.id$$

Lean4

@[simp]
theorem isTrivial_def (ρ : Representation k G V) [IsTrivial ρ] (g : G) : ρ g = LinearMap.id :=
  IsTrivial.out g

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

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

Разделы

Аффилиация

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