Structures · Algebra
IsSemisimpleModule
A module is semisimple when every submodule has a complement, or equivalently, the module is a direct sum of simple modules.
- Defined in
- Mathlib.RingTheory.SimpleModule.Basic
- Shape
- 2 explicit arguments
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- MonoidAlgebra
How is a type an instance?
Loading the hierarchy index…
Assumed by62
- IsSemisimpleModule.congr
- IsSemisimpleModule.eq_bot_or_exists_simple_le
- IsSemisimpleModule.annihilator_isRadical
- IsSemisimpleModule.jacobson_eq_bot
- IsSemisimpleModule.sSup_simples_eq_top
- OrderIso.setIsotypicComponents
- IsSemisimpleModule.exists_linearEquiv_dfinsupp
- IsIsotypic.linearEquiv_fun
- IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end
- isFullyInvariant_iff_le_imp_isotypicComponent_le
- Submodule.le_linearEquiv_of_sSup_eq_top
- IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top
- IsSemisimpleModule.of_injective
- IsSemisimpleModule.extension_property
- IsSemisimpleModule.finite_tfae
- IsSemisimpleModule.sSup_simples_le
- Submodule.le_linearEquiv_of_le_sSup
- le_isotypicComponent_iff
- IsIsotypicOfType.linearEquiv_fun
- IsSemisimpleModule.exists_submodule_linearEquiv_quotient
- IsSemisimpleModule.lifting_property
- eq_isotypicComponent_iff
- IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp
- IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing
- IsIsotypicOfType.linearEquiv_finsupp
- LinearMap.linearEquiv_of_ne_zero
- IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing
- IsSemisimpleModule.endAlgEquiv
- IsIsotypic.submodule_linearEquiv_fun
- jacobson_density
- isFullyInvariant_iff_sSup_isotypicComponents
- isotypicComponent_eq_top_iff
- IsSemisimpleModule.instIsNoetherianOfFinite
- Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule
- OrderIso.setIsotypicComponents_apply
- instIsSemisimpleModuleForallOfFinite
- instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent
- instIsSemisimpleModuleFinsupp
- Module.End.isSemisimple_zero
- IsSemisimpleModule.isCoatomic_submodule
- IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end
- sSup_isotypicComponents
- OrderIso.setIsotypicComponents_symm_apply
- Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1
- Module.Finite.toModuleEnd_moduleEnd_surjective
- IsSemisimpleModule.exists_quotient_linearEquiv_submodule
- IsSemisimpleModule.submodule
- instIsArtinianOfIsSemisimpleModuleOfFinite
- mem_isotypicComponents_iff
- IsSemisimpleModule.exists_simple_submodule