rank_pos

Mathlib.LinearAlgebra.Dimension.Finite

URI: https://scilib.ai/kg/mathlib#rank_pos

English

If the rank of a submodule s ⊆ M is positive, then s contains a nonzero element.

Русский

Если ранг подмодуля s над M положителен, то в s есть ненулевой элемент.

LaTeX

$$$\operatorname{rank}_R s > 0 \Rightarrow \exists b \in s, b \neq 0.$$$

Lean4

theorem rank_pos [Nontrivial M] : 0 < Module.rank R M :=
  rank_pos_iff_nontrivial.mpr ‹_›

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

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

Разделы

Аффилиация

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