rank_zero_iff_forall_zero — Mathlib

English

Under NoZeroSMulDivisors and nontrivial R, rank R M = 0 if and only if every x ∈ M is zero (i.e., M is the trivial module).

Русский

При NoZeroSMulDivisors и ненулевом кольце R, ранг равен нулю тогда и только тогда каждый вектор равен нулю.

LaTeX

$$$\operatorname{rank}_R M = 0 \iff \forall x \in M, x = 0.$$$

Lean4

theorem rank_zero_iff_forall_zero : Module.rank R M = 0 ↔ ∀ x : M, x = 0 := by
  simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or, exists_and_right,
    and_iff_right (exists_ne (0 : R))]

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