length_pos

Mathlib.RingTheory.Length

URI: https://scilib.ai/kg/mathlib#Module.length_pos

English

If M is nontrivial, then 0 < Module.length R M.

Русский

Если M не тривиален, то 0 < длина модуля.

LaTeX

$$$[\operatorname{Nontrivial} M] \Rightarrow 0 < \operatorname{length}(R,M).$$$

Lean4

theorem length_pos [Nontrivial M] : 0 < Module.length R M :=
  Module.length_pos_iff.mpr ‹_›

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

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

Разделы

Аффилиация

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