rank_le_one_iff_top_isPrincipal — Mathlib

English

The whole module has rank at most 1 iff the top submodule is principal.

Русский

Вся модуль имеет ранг не более 1 тогда и только тогда, когда верхний подмодуль главный.

LaTeX

$$$$ Module.rank\\,K\\,V \\le 1 \\iff (\\top : Submodule K V).IsPrincipal $$$$

Lean4

theorem rank_le_one_iff_top_isPrincipal [Module.Free K V] : Module.rank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal :=
  by
  haveI := Module.Free.of_equiv (topEquiv (R := K) (M := V)).symm
  rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]

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