English
If ker f is nilpotent and each e i is idempotent and central, and f ∘ e is a complete orthogonal idempotents, then e is a complete orthogonal idempotents as well.
Русский
Если ядро f нильпотентно, каждый e_i идempotент и центральен, и f ∘ e является полной ортогональной цепью идемпотентов, то e тоже образует полную ортогональную систему идемпотентов.
LaTeX
$$$(h : ∀ x ∈ \\ker f, IsNilpotent x) \\Rightarrow (he : \\forall i, IsIdempotentElem (e i)) \\Rightarrow (he' : ∀ i, IsMulCentral (e i)) \\Rightarrow (he'' : CompleteOrthogonalIdempotents (f ∘ e)) \\Rightarrow CompleteOrthogonalIdempotents e$$$
Lean4
theorem of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (he : ∀ i, IsIdempotentElem (e i))
(he' : CompleteOrthogonalIdempotents (f ∘ e)) : CompleteOrthogonalIdempotents e :=
of_ker_isNilpotent_of_isMulCentral f h he (fun _ ↦ Semigroup.mem_center_iff.mpr (mul_comm · _)) he'
