Mathlib.LinearAlgebra.Semisimple._auxLemma.2

theorem Mathlib.LinearAlgebra.Semisimple._auxLemma.2 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}, f.IsSemisimple = ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q

The theorem `Mathlib.LinearAlgebra.Semisimple._auxLemma.2` states that for any commutative ring `R`, additive commutative group `M` and `R`-module structure on `M`, a linear endomorphism `f` of the `R`-module `M` is semisimple if and only if for any `R`-submodule `p` of `M` that is `f`-invariant (i.e., `p` is less than or equal to the preimage of `p` under `f`), there exists an `f`-invariant `R`-submodule `q` of `M` such that `p` and `q` are complementary, i.e., their sum is the whole module and their intersection is trivial.

More concisely: A linear endomorphism of an `R`-module is semisimple if and only if for every `f`-invariant `R`-submodule, there exists a complementary `f`-invariant submodule.