finrank_le_one_iff_top_isPrincipal

English

For a finite-dimensional free module V over K, finrank K V ≤ 1 if and only if the top submodule (the entire space) is principal.

Русский

Для конечномодульного свободного пространства V над K выполнено: финразмерность V ≤ 1 тогда и только тогда, когда верхнее подпространство (всё пространство) является порожденным одним элементом.

LaTeX

$$$\operatorname{finrank} K V \le 1 \iff (\top : \text{Submodule } K V).IsPrincipal$$$

Lean4

theorem finrank_le_one_iff_top_isPrincipal [Module.Free K V] [Module.Finite K V] :
    finrank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal := by
  rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

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