rank_le_one_iff_isPrincipal — Mathlib

English

A submodule has rank at most 1 iff it is principal.

Русский

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

LaTeX

$$$$ (\\text{rank}_K s) \\le 1 \\iff s.IsPrincipal $$$$

Lean4

theorem rank_le_one_iff_isPrincipal (W : Submodule K V) [Module.Free K W] : Module.rank K W ≤ 1 ↔ W.IsPrincipal :=
  by
  simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
    span_singleton_le_iff_mem]
  constructor
  · rintro ⟨⟨m, hm⟩, hm'⟩
    choose f hf using hm'
    exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩
  · rintro ⟨a, ⟨h, ha⟩⟩
    choose f hf using h
    exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

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