isProj_averageMap

Mathlib.RepresentationTheory.Invariants

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

English

averageMap is a projection from the whole space onto invariants.

Русский

averageMap является проекцией пространства на инварианты.

LaTeX

$$$$ \text{averageMap}: V \to \mathrm{invariants}\;\rho \text{ is a projection.} $$$$

Lean4

theorem isProj_averageMap : LinearMap.IsProj ρ.invariants ρ.averageMap :=
  ⟨ρ.averageMap_invariant, ρ.averageMap_id⟩

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

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

Разделы

Аффилиация

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