finite_basis — Mathlib

English

If M is finite over R and R is nontrivial, then any basis ι → M has finite index ι.

Русский

Если M конечно над R и R не тривиально, то любая база ι → M имеет конечный индекс ι.

LaTeX

$$$[Module.Finite R M] \Rightarrow [\text{Nontrivial } R] \Rightarrow Finite ι \text{ for any basis } b: ι \to M.$$$

Lean4

/-- If a free module is finite, then any arbitrary basis is finite. -/
theorem finite_basis [Nontrivial R] {ι} [Module.Finite R M] (b : Basis ι R M) : _root_.Finite ι :=
  let ⟨s, hs⟩ := ‹Module.Finite R M›
  basis_finite_of_finite_spans s.finite_toSet hs b

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