instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule

Mathlib.LinearAlgebra.RootSystem.Irreducible

URI: https://scilib.ai/kg/mathlib#RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule

English

If M is nontrivial, then P.invtRootSubmodule is a nontrivial subtype-subset of Submodule M.

Русский

Если M ненулевой, то P.invtRootSubmodule образует ненулевое подподмножество Submodule M.

LaTeX

$$$$ \text{Nontrivial } P.invtRootSubmodule $$$$

Lean4

instance [Nontrivial M] : Nontrivial P.invtRootSubmodule where
  exists_pair_ne := ⟨⊥, ⊤, by rw [ne_eq, Subtype.ext_iff]; exact bot_ne_top⟩

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

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

Разделы

Аффилиация

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