instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent

English

For any isotypic component c in isotypicComponents, the subtype with c.val membership is nontrivial.

Русский

Для любого компонента изотипичности c из isotypicComponents, подвклад c.val не тривиален.

LaTeX

$$$\text{Nontrivial} (Subtype\ (fun x => SetLike.instMembership.mem c.val x))$$$

Lean4

instance [IsSemisimpleModule R S] : IsSemisimpleModule R (isotypicComponent R M S) :=
  by
  rw [isotypicComponent, sSup_eq_iSup]
  refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_
  have := IsSemisimpleModule.congr e
  infer_instance

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