finite_of_rank_eq_zero — Mathlib

English

If NoZeroSMulDivisors holds and rank R M = 0, then M is finite.

Русский

Если выполняются NoZeroSMulDivisors и ранг равен нулю, то M конечно.

LaTeX

$$$[\text{NoZeroSMulDivisors } R M] \land \operatorname{rank}_R M = 0 \Rightarrow \text{Module.Finite } R M.$$$

Lean4

theorem finite_of_rank_eq_zero [NoZeroSMulDivisors R M] (h : Module.rank R M = 0) : Module.Finite R M :=
  by
  nontriviality R
  rw [rank_zero_iff] at h
  infer_instance

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