isSemisimpleModule_of_isSemisimpleModule_submodule'

English

Given a family of semisimple submodules, the generated submodule is semisimple.

Русский

Из семейства полупрямых подмодулей порожденный ею подмодуль полупрямой.

LaTeX

$$isSemisimpleModule_of_isSemisimpleModule_submodule' hp hp'$$

Lean4

theorem isSemisimpleModule_of_isSemisimpleModule_submodule' {p : ι → Submodule R M}
    (hp : ∀ i, IsSemisimpleModule R (p i)) (hp' : ⨆ i, p i = ⊤) : IsSemisimpleModule R M :=
  isSemisimpleModule_of_isSemisimpleModule_submodule (s := Set.univ) (fun i _ ↦ hp i) (by simpa)

Похожие утверждения