rank_submodule_le_one_iff — Mathlib

English

A submodule has rank at most 1 iff there exists v0 in s with s ≤ span{v0}.

Русский

Подмодуль обладает рангом не более 1 тогда и только тогда, когда существует v0 в s с условием s ⊆ span{v0}.

LaTeX

$$$$ Module.rank\\,K\\,s \\le 1 \\iff \\exists v_0 \\in s, s \\le K \\cdot v_0 $$$$

Lean4

/-- A submodule has dimension at most `1` if and only if there is a
single vector in the submodule such that the submodule is contained in
its span. -/
theorem rank_submodule_le_one_iff (s : Submodule K V) [Module.Free K s] : Module.rank K s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀ :=
  by
  simp_rw [rank_le_one_iff, le_span_singleton_iff]
  simp

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