finrank_eq_zero — Mathlib

English

Within Submodule, finrank R S is zero if and only if S equals ⊥, under standard finiteness conditions.

Русский

В рамках подмодуля finrank_R(S) равен нулю тогда и только тогда, когда S = ⊥, при обычных условиях конечности.

LaTeX

$$$$\\\\operatorname{finrank}_R S = 0 \\\\iff S = \\\\bot.$$$$

Lean4

@[simp]
theorem finrank_eq_zero [StrongRankCondition R] [NoZeroSMulDivisors R M] {S : Submodule R M} [Module.Finite R S] :
    finrank R S = 0 ↔ S = ⊥ := by
  rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]

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