instInhabitedAsModule

Mathlib.RepresentationTheory.Basic

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

English

If a representation is IsTrivial, then all its images are the identity maps.

Русский

Если представление IsTrivial, то все его изображения являются тождественными отображениями.

LaTeX

$$IsTrivial ρ ⇒ ∀ g, ρ g = id$$

Lean4

instance : Inhabited ρ.asModule where default := 0

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

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

Разделы

Аффилиация

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