basis_finite_of_finite_spans — Mathlib

English

If there exists a finite spanning set, then any basis must be finite.

Русский

Если существует конечный порождающий набор, то любой базис конечен.

LaTeX

$$$\\text{Finite}(s) \\land span\\ R\\ s = \\top \\Rightarrow \\text{Finite}(\\iota)$ for any basis ι R M$$

Lean4

/-- Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
-/
theorem basis_finite_of_finite_spans [Nontrivial R] {s : Set M} (hs : s.Finite) (hsspan : span R s = ⊤) {ι : Type w}
    (b : Basis ι R M) : Finite ι := by
  have := congr(($hsspan).map b.repr)
  rw [← span_image, Submodule.map_top, LinearEquivClass.range] at this
  exact finite_of_span_finite_eq_top_finsupp (hs.image _) this

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