instNontrivial

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.instNontrivial

English

If M is nontrivial, then LieSubmodule R L M is nontrivial.

Русский

Если M ненулевой, то Ли-подмодульная система ненулевая.

LaTeX

$$Nontrivial M \\Rightarrow Nontrivial (LieSubmodule R L M)$$

Lean4

instance [Nontrivial M] : Nontrivial (LieSubmodule R L M) :=
  (nontrivial_iff R L M).mpr ‹_›

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

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

Разделы

Аффилиация

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