instNontrivial

Mathlib.Algebra.Module.Submodule.Lattice

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

English

If M is nontrivial, then the module of submodules Submodule R M is nontrivial.

Русский

Если M не тривиален, то множество подмодулей Submodule R M также не тривиально.

LaTeX

$$$\\text{Nontrivial}(M) \\Rightarrow \\text{Nontrivial}(\\text{Submodule } R M)$$$

Lean4

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

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

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

Разделы

Аффилиация

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