one_le_finrank_iff — Mathlib

English

For a submodule S, 1 ≤ finrank_R(S) if and only if S ≠ ⊥.

Русский

Для подмодуля S верно: 1 ≤ finrank_R(S) тогда и только тогда, когда S ≠ ⊥.

LaTeX

$$$$1 \\\\le \\\\operatorname{finrank}_R S \\\\iff S \\\\neq \\\\bot.$$$$

Lean4

@[simp]
theorem one_le_finrank_iff [StrongRankCondition R] [NoZeroSMulDivisors R M] {S : Submodule R M} [Module.Finite R S] :
    1 ≤ finrank R S ↔ S ≠ ⊥ := by simp [← not_iff_not]

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