not_finite_of_infinite_basis — Mathlib

English

If the index set ι of a basis is infinite, then the module M is not finite.

Русский

Если множество индексов основания бесконечно, то модуль не конечен.

LaTeX

$$$[\text{Infinite } ι] \Rightarrow ¬ Finite M \text{ for any basis } b: ι \to M.$$$

Lean4

theorem not_finite_of_infinite_basis [Nontrivial R] {ι} [Infinite ι] (b : Basis ι R M) : ¬Module.Finite R M := fun _ ↦
  (Finite.finite_basis b).not_infinite ‹_›

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