LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo

theorem LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {Φ : Set M}, Φ.Finite → Submodule.span R Φ = ⊤ → ∀ {e : M ≃ₗ[R] M}, Set.MapsTo (⇑e) Φ Φ → IsOfFinOrder e

This theorem states that for a given commutative semiring `R` and an additive commutative monoid `M` which is also a module over `R`, if there is a linear equivalence `e` that maps a finite set `Φ` to itself such that the span of `Φ` equals the entire module `M`, then `e` must have finite order. In other words, there exists a positive integer `n` such that applying `e` `n` times to any element results in the original element. Essentially, it is stating that a linear transformation that preserves a finite spanning set of a module must be periodic.

More concisely: If `R` is a commutative semiring, `M` is a commutative `R`-module with a finite spanning set `Φ` and there exists a linear equivalence `e` on `M` mapping `Φ` to itself, then `e` has finite order.