rank_subsingleton' — Mathlib

English

If the type M is a subsingleton (has at most one element), then Module.rank R M = 0.

Русский

Если тип M является одиночным (Subsingleton), то Module.rank R M = 0.

LaTeX

$$$\\operatorname{Module.rank} R M = 0$$$

Lean4

/-- See `rank_subsingleton` that assumes `Subsingleton R` instead. -/
@[simp, nontriviality]
theorem rank_subsingleton' [Subsingleton M] : Module.rank R M = 0 :=
  by
  rw [Module.rank, ← bot_eq_zero, eq_bot_iff]
  exact ciSup_le fun s ↦ by simp [(linearIndependent_subsingleton_iff _).mp s.2]

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