English
IsFinitelySemisimple(f) iff for every invariant p with hp, p finite implies the analogous condition for all q ≤ p.
Русский
IsFinitelySemisimple(f) эквивалентно условию на инвариантных p: если p конечно, то выполняется соответствующее условие для всех q ≤ p.
LaTeX
$$$$ f.IsFinitelySemisimple \\iff \\forall p \\in invtSubmodule f, \\ Module.Finite R p \\rightarrow \\ \\forall q \\in invtSubmodule f, q \\le p \\rightarrow \\ exists r \\le p, r \\le p \\land r \\in invtSubmodule f \\land Disjoint q r \\land q \\sqcup r = p. $$$$
Lean4
/-- A linear endomorphism is finitely semisimple if it is semisimple on every finitely-generated
invariant submodule.
See also `Module.End.isFinitelySemisimple_iff`. -/
theorem isFinitelySemisimple_iff' :
f.IsFinitelySemisimple ↔
∀ p (hp : p ∈ invtSubmodule f), Module.Finite R p → IsSemisimple (LinearMap.restrict f hp) :=
Iff.rfl
