Structures · Algebra
IsSimpleModule
A module is simple when it has only two submodules, ⊥ and ⊤.
- Defined in
- Mathlib.RingTheory.SimpleModule.Basic
- Shape
- 2 explicit arguments
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- MonoidAlgebra
- Module.End
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- IsSimpleModule.congr
- IsSimpleModule.nontrivial
- Submodule.IsFullyInvariant.isotypicComponent
- IsIsotypicOfType.isotypicComponent
- IsSimpleModule.toSpanSingleton_surjective
- LinearMap.bijective_or_eq_zero
- LinearMap.injective_or_eq_zero
- bot_lt_isotypicComponent
- LinearMap.surjective_or_eq_zero
- Submodule.le_linearEquiv_of_sSup_eq_top
- IsIsotypic.isotypicComponent
- IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed
- Submodule.map_le_isotypicComponent
- Module.length_eq_one
- Submodule.le_linearEquiv_of_le_sSup
- le_isotypicComponent_iff
- IsSimpleModule.jacobson_eq_bot
- IsSimpleModule.span_singleton_eq_top
- LinearMap.isClosed_or_dense_ker
- eq_isotypicComponent_iff
- LinearMap.isCoatom_ker_of_surjective
- Submodule.linearEquiv_of_sSup_eq_top
- LinearMap.surjective_of_ne_zero
- LinearMap.injective_of_ne_zero
- eq_isotypicComponent_of_le
- LinearMap.linearEquiv_of_ne_zero
- IsSimpleModule.annihilator_isMaximal
- IsSimpleModule.ker_toSpanSingleton_isMaximal
- IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule
- LinearMap.le_comap_isotypicComponent
- IsSimpleModule.finrank_eq_one_of_isMulCommutative
- Submodule.linearEquiv_of_le_sSup
- isotypicComponent_eq_top_iff
- instIsSimpleModuleSubtypeMemSubmoduleValSetOfPredNonemptyLinearEquivId
- IsSimpleModule.instIsPrincipal
- IsSimpleModule.instIsNoetherian
- IsIsotypicOfType.of_isotypicComponent_eq_top
- IsSimpleModule.obj_of_isEquivalence
- IsSimpleModule.toIsSimpleOrder
- LinearMap.bijective_of_ne_zero
- simple_of_isSimpleModule
- IsSimpleModule.isAtom
- IsIsotypicOfType.of_isSimpleModule
- Module.End.instDivisionRing
- DivisionRing.nonempty_linearEquiv_of_isSimpleModule
- instIsSemisimpleModuleOfIsSimpleModule