finrank_eq_zero_of_not_exists_basis

English

If there does not exist any basis (on any subset) for M, then finrank_R(M) = 0.

Русский

Если не существует вообще ни одной базы для M, то finrank_R(M) = 0.

LaTeX

$$$$ \\lnot \\exists S \\subseteq M,\\text{Basis}(S) \\\\Rightarrow \\\\operatorname{finrank}_R M = 0.$$$$

Lean4

theorem finrank_eq_zero_of_not_exists_basis (h : ¬∃ s : Finset M, Nonempty (Basis (s : Set M) R M)) : finrank R M = 0 :=
  finrank_eq_zero_of_basis_imp_false fun s b => h ⟨s, ⟨b⟩⟩

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