rank_subsingleton — Mathlib

English

If the ring R is a subsingleton, then Module.rank R M = 1 for any nontrivial M.

Русский

Если кольцо R является одиночным, то для любого ненулевого M размера ранг равен 1.

LaTeX

$$[Subsingleton R] ⇒ Module.rank R M = 1$$

Lean4

@[nontriviality, simp]
theorem rank_subsingleton [Subsingleton R] : Module.rank R M = 1 :=
  by
  haveI := Module.subsingleton R M
  have : Nonempty { s : Set M // LinearIndepOn R id s } := ⟨⟨∅, linearIndepOn_empty _ _⟩⟩
  rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
  · rintro ⟨s, hs⟩
    rw [Cardinal.mk_le_one_iff_set_subsingleton]
    apply Set.subsingleton_of_subsingleton
  intro w hw
  exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

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