finrank_eq_zero_of_basis_imp_false

English

If there does not exist a finite basis for M, then finrank_R(M) = 0.

Русский

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

LaTeX

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

Lean4

theorem finrank_eq_zero_of_basis_imp_false (h : ∀ s : Finset M, Basis.{v} (s : Set M) R M → False) : finrank R M = 0 :=
  finrank_eq_zero_of_basis_imp_not_finite fun s b hs =>
    h hs.toFinset
      (by
        convert b
        simp)

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