Additional results about finite spanning sets in linear algebra #
theorem
LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{Φ : Set M}
(hΦ₁ : Φ.Finite)
(hΦ₂ : Submodule.span R Φ = ⊤)
{e : M ≃ₗ[R] M}
(he : Set.MapsTo (⇑e) Φ Φ)
:
A linear equivalence which preserves a finite spanning set must have finite order.