English
IsFinitelySemisimple(f) iff for all p ∈ invtSubmodule f, the finite p condition implies the lattice-theoretic property stated.
Русский
IsFinitelySemisimple(f) эквивалентно выполнению конечного условия на p в invtSubmodule f и связанному свойству решетки.
LaTeX
$$$$ f.IsFinitelySemisimple \\iff \\forall p (hp : p \\in invtSubmodule f), Module.Finite R p \\rightarrow \\forall (q : Submodule R M), q \\in invtSubmodule f \\rightarrow ( \\text{le } q p \\rightarrow \\exists r \\le p, r \\in invtSubmodule f \\land Disjoint q r \\land q \\sqcup r = p ). $$$$
Lean4
/-- A characterisation of `Module.End.IsFinitelySemisimple` using only the lattice of submodules of
`M` (thus avoiding submodules of submodules). -/
theorem isFinitelySemisimple_iff :
f.IsFinitelySemisimple ↔
∀ p ∈ invtSubmodule f,
Module.Finite R p →
∀ q ∈ invtSubmodule f, q ≤ p → ∃ r, r ≤ p ∧ r ∈ invtSubmodule f ∧ Disjoint q r ∧ q ⊔ r = p :=
by simp_rw [isFinitelySemisimple_iff', isSemisimple_restrict_iff]
