nontrivial_of_isIrreducible

Mathlib.Algebra.Lie.Semisimple.Basic

URI: https://scilib.ai/kg/mathlib#LieModule.nontrivial_of_isIrreducible

← MathLib Explorer

English

If a Lie module M is irreducible, then M is nontrivial.

Русский

Если модуль Ли необразуем, то он не тривиален.

LaTeX

$$$$ \\text{IsIrreducible } R L M \\Rightarrow \\text{Nontrivial } M $$$$

Lean4

theorem nontrivial_of_isIrreducible [LieModule.IsIrreducible R L M] : Nontrivial M where
  exists_pair_ne := by
    have aux : (⊥ : LieSubmodule R L M) ≠ ⊤ := bot_ne_top
    contrapose! aux
    ext m
    simpa using aux m 0

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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