exists_mem_ne_zero_of_rank_pos — Mathlib

English

If rank of a submodule s is positive, there exists a nonzero member in s; this is a restatement of the previous lemma in a different formulation.

Русский

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

LaTeX

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

Lean4

theorem exists_mem_ne_zero_of_rank_pos {s : Submodule R M} (h : 0 < Module.rank R s) : ∃ b : M, b ∈ s ∧ b ≠ 0 :=
  exists_mem_ne_zero_of_ne_bot fun eq => by rw [eq, rank_bot] at h; exact lt_irrefl _ h

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