Documentation

Mathlib.LinearAlgebra.FiniteSpan

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.