finrank_eq_zero_iff — Mathlib

English

Another articulation of finrank zero condition with vector annihilators.

Русский

Еще одно формулировочное выражение условия нуля finrank через аннигилирующие скаляры.

LaTeX

$$$\operatorname{finrank} R M = 0 \iff \forall x \in M, \exists a \neq 0, a x = 0$$$

Lean4

/-- See `Module.finrank_zero_iff`
  for the stronger version with `NoZeroSMulDivisors R M`. -/
theorem finrank_eq_zero_iff : finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 :=
  by
  rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]
  norm_cast

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