English
Let N be a submodule of M with rank smaller than that of M. Then there exists m ∈ M such that for every nonzero r ∈ R, the element r·m is not in N.
Русский
Пусть N — подслагаемое подмодуля M и ранк N строго меньше ранга M. Существует m ∈ M, для которого для любого ненулевого r ∈ R верно: r·m ∉ N.
LaTeX
$$$\text{If } N \le M \text{ with } \operatorname{rank}_R N < \operatorname{rank}_R M, \ \exists m \in M\text{ such that } \forall r \in R\setminus\{0\},\ r\cdot m \notin N. $$$
Lean4
theorem exists_smul_notMem_of_rank_lt {N : Submodule R M} (h : Module.rank R N < Module.rank R M) :
∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N :=
by
have : Module.rank R (M ⧸ N) ≠ 0 := by
intro e
rw [← rank_quotient_add_rank N, e, zero_add] at h
exact h.ne rfl
rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this
push_neg at this
simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this
exact this
