Basic

📁 Source: Mathlib/RingTheory/SimpleModule/Basic.lean

Statistics

Metric	Count
Definitions `IsSemisimpleModule`, `IsSemisimpleRing`, `IsSimpleModule`, `instJordanHolderLattice`, `instDivisionRing`	5
Theorems `annihilator_isRadical`, `eq_bot_or_exists_simple_le`, `exists_linearEquiv_dfinsupp`, `exists_linearEquiv_fin_dfinsupp`, `exists_quotient_linearEquiv_submodule`, `exists_sSupIndep_sSup_simples_eq_top`, `exists_simple_submodule`, `exists_submodule_linearEquiv_quotient`, `extension_property`, `instIsNoetherianOfFinite`, `isCoatomic_submodule`, `lifting_property`, `of_injective`, `of_sSup_simples_eq_top`, `of_surjective`, `quotient`, `range`, `sSup_simples_eq_top`, `sSup_simples_le`, `submodule`, `sup`, `toComplementedLattice`, `exists_linearEquiv_ideal_of_isSimpleModule`, `ideal_eq_span_idempotent`, `isSemisimpleModule`, `annihilator_isMaximal`, `instIsNoetherian`, `instIsPrincipal`, `isAtom`, `ker_toSpanSingleton_isMaximal`, `nontrivial`, `span_singleton_eq_top`, `toIsSimpleOrder`, `toSpanSingleton_surjective`, `isSemisimpleModule_iff`, `isSimpleModule_iff`, `bijective_of_ne_zero`, `bijective_or_eq_zero`, `injective_of_ne_zero`, `injective_or_eq_zero`, `instIsSimpleModuleEndOfNontrivial`, `isCoatom_ker_of_surjective`, `isSemisimpleModule_iff_of_bijective`, `isSimpleModule_iff_of_bijective`, `linearEquiv_of_ne_zero`, `surjective_of_ne_zero`, `surjective_or_eq_zero`, `instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule`, `instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1`, `of_isComplemented_codomain`, `of_isComplemented_domain`, `toModuleEnd_moduleEnd_surjective`, `isSemisimpleRing`, `isSemisimpleRing_iff`, `isSemisimpleRing_of_surjective`, `covBy_iff_quot_is_simple`, `instIsPrincipalIdealRingOfIsSemisimpleRing`, `instIsSemisimpleModuleDFinsupp`, `instIsSemisimpleModuleFinsupp`, `instIsSemisimpleModuleForallOfFinite`, `instIsSemisimpleModuleOfIsSimpleModule`, `instIsSemisimpleRingForallOfFinite`, `instIsSemisimpleRingOfSubsingleton`, `instIsSemisimpleRingProd`, `instIsSimpleModule`, `isSemisimpleModule_biSup_of_isSemisimpleModule_submodule`, `isSemisimpleModule_iff`, `isSemisimpleModule_iff_exists_linearEquiv_dfinsupp`, `isSemisimpleModule_of_isSemisimpleModule_submodule`, `isSemisimpleModule_of_isSemisimpleModule_submodule'`, `isSimpleModule_iff`, `isSimpleModule_iff_isAtom`, `isSimpleModule_iff_isCoatom`, `isSimpleModule_iff_quot_maximal`, `isSimpleModule_iff_toSpanSingleton_surjective`, `isSimpleModule_self_iff_isUnit`, `jacobson_density`, `sSup_simples_eq_top_iff_isSemisimpleModule`	78
Total	83

IsSemisimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`annihilator_isRadical` 📖	mathematical	—	`Ideal.IsRadical` `CommRing.toCommSemiring` `Module.annihilator` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Submodule.annihilator_top` `sSup_simples_eq_top` `sSup_eq_iSup'` `Submodule.annihilator_iSup` `Ideal.isRadical_iInf` `Ideal.IsPrime.isRadical` `Ideal.IsMaximal.isPrime` `IsSimpleModule.annihilator_isMaximal`
`eq_bot_or_exists_simple_le` 📖	mathematical	—	`Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`Submodule.subsingleton_iff_eq_bot` `Submodule.subsingleton_iff` `subsingleton_iff_bot_eq_top` `RingHomSurjective.ids` `Submodule.map_subtype_le` `IsSimpleModule.congr` `RingHomSurjective.invPair` `RingHomInvPair.ids` `Submodule.subtype_injective` `isSimpleModule_iff_isAtom` `IsAtomic.eq_bot_or_exists_atom_le` `isAtomic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `toComplementedLattice`
`exists_linearEquiv_dfinsupp` 📖	mathematical	—	`sSupIndep` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Set` `Set.instMembership` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomInvPair.ids` `exists_sSupIndep_sSup_simples_eq_top` `RingHomSurjective.invPair` `AddMonoid.nat_smulCommClass'` `RingHomCompTriple.ids` `iSupIndep.dfinsupp_lsum_injective` `sSupIndep_iff` `RingHomSurjective.ids` `Submodule.iSup_eq_range_dfinsupp_lsum` `sSup_eq_iSup'` `SetCoe.forall`
`exists_linearEquiv_fin_dfinsupp` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomInvPair.ids` `exists_linearEquiv_dfinsupp` `WellFoundedGT.finite_of_iSupIndep` `wellFoundedGT` `instIsNoetherianOfFinite` `sSupIndep_iff` `Submodule.nontrivial_iff_ne_bot` `IsSimpleModule.nontrivial` `RingHomCompTriple.ids`
`exists_quotient_linearEquiv_submodule` 📖	mathematical	—	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.addCommMonoid` `Submodule.Quotient.addCommGroup` `Submodule.module` `Submodule.Quotient.module`	—	`RingHomInvPair.ids` `ComplementedLattice.exists_isCompl` `toComplementedLattice` `IsCompl.symm`
`exists_sSupIndep_sSup_simples_eq_top` 📖	mathematical	—	`sSupIndep` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `Submodule.instTop` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`sSup_simples_eq_top` `exists_sSupIndep_of_sSup_atoms_eq_top` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated`
`exists_simple_submodule` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`IsAtomic.exists_atom` `Submodule.instNontrivial` `isAtomic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `toComplementedLattice`
`exists_submodule_linearEquiv_quotient` 📖	mathematical	—	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.addCommMonoid` `Submodule.Quotient.addCommGroup` `Submodule.module` `Submodule.Quotient.module`	—	`RingHomInvPair.ids` `ComplementedLattice.exists_isCompl` `toComplementedLattice`
`extension_property` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `ComplementedLattice.exists_isCompl` `toComplementedLattice` `LinearMap.ext` `LinearMap.linearProjOfIsCompl_apply_left`
`instIsNoetherianOfFinite` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `exists_quotient_linearEquiv_submodule` `Submodule.FG.of_finite` `Module.Finite.equiv` `Module.Finite.quotient`
`isCoatomic_submodule` 📖	mathematical	—	`IsCoatomic` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderTop`	—	`isCoatomic_of_isAtomic_of_complementedLattice_of_isModular` `Submodule.instIsModularLattice` `toComplementedLattice` `isAtomic_of_complementedLattice` `Submodule.instIsCompactlyGenerated`
`lifting_property` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `ComplementedLattice.exists_isCompl` `toComplementedLattice` `RingHomInvPair.ids` `LinearMap.ext` `LinearEquiv.surjective` `LinearEquiv.symm_apply_apply`
`of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsSemisimpleModule`	—	`congr` `RingHomSurjective.invPair` `RingHomInvPair.ids` `submodule` `RingHomCompTriple.ids`
`of_sSup_simples_eq_top` 📖	mathematical	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `setOf` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Top.top` `Submodule.instTop`	`IsSemisimpleModule`	—	`complementedLattice_of_sSup_atoms_eq_top` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated`
`of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsSemisimpleModule`	—	`congr` `quotient` `RingHomInvPair.ids`
`quotient` 📖	mathematical	—	`IsSemisimpleModule` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`RingHomInvPair.ids` `exists_submodule_linearEquiv_quotient` `congr` `submodule`
`range` 📖	mathematical	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommGroup` `Submodule.module`	—	`congr` `RingHomSurjective.ids` `quotient` `RingHomInvPair.ids`
`sSup_simples_eq_top` 📖	mathematical	—	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `setOf` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Top.top` `Submodule.instTop`	—	`sSup_atoms_eq_top` `isAtomistic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `toComplementedLattice`
`sSup_simples_le` 📖	mathematical	—	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `setOf` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`sSup_atoms_le_eq` `isAtomistic_of_complementedLattice` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `toComplementedLattice`
`submodule` 📖	mathematical	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	—	`OrderIso.complementedLattice_iff` `IsModularLattice.complementedLattice_Iic` `Submodule.instIsModularLattice` `toComplementedLattice`
`sup` 📖	mathematical	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.addCommGroup` `Submodule.module`	—	`iSup_univ` `iSup_bool_eq` `isSemisimpleModule_biSup_of_isSemisimpleModule_submodule`
`toComplementedLattice` 📖	mathematical	—	`ComplementedLattice` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `CompleteLattice.toBoundedOrder`	—	—

IsSemisimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_linearEquiv_ideal_of_isSimpleModule` 📖	mathematical	—	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomInvPair.ids` `isSimpleModule_iff_quot_maximal` `IsSemisimpleModule.exists_submodule_linearEquiv_quotient` `RingHomCompTriple.ids`
`ideal_eq_span_idempotent` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal.span` `Ring.toSemiring` `Set` `Set.instSingletonSet`	—	`ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice` `RingHomSurjective.ids` `LinearMap.isIdempotentElem_map_one_iff` `LinearMap.range_eq_map` `Ideal.span_one` `Ideal.submodule_span_eq` `LinearMap.map_span` `Set.image_one`
`isSemisimpleModule` 📖	mathematical	—	`IsSemisimpleModule`	—	`IsSemisimpleModule.congr` `IsSemisimpleModule.quotient` `instIsSemisimpleModuleFinsupp` `RingHomInvPair.ids` `Finsupp.linearCombination_id_surjective`

IsSimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`annihilator_isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.annihilator` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids` `isSimpleModule_iff_quot_maximal` `LinearEquiv.annihilator_eq` `Ideal.annihilator_quotient` `Ideal.instIsTwoSided_1`
`instIsNoetherian` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`isNoetherian_iff'` `Finite.to_wellFoundedGT` `IsSimpleOrder.instFinite` `toIsSimpleOrder`
`instIsPrincipal` 📖	mathematical	—	`Submodule.IsPrincipal` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsSimpleOrder.eq_bot_or_eq_top` `toIsSimpleOrder` `Submodule.span_zero` `nontrivial` `exists_ne` `span_singleton_eq_top`
`isAtom` 📖	mathematical	—	`IsAtom` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instOrderBot`	—	`isSimpleModule_iff_isAtom`
`ker_toSpanSingleton_isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `Ring.toSemiring` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Semiring.toModule` `RingHom.id` `LinearMap.toSpanSingleton`	—	`Ideal.isMaximal_def` `isSimpleModule_iff_isCoatom` `congr` `toSpanSingleton_surjective`
`nontrivial` 📖	mathematical	—	`Nontrivial`	—	`bot_ne_top` `IsSimpleOrder.toNontrivial` `toIsSimpleOrder` `Mathlib.Tactic.Contrapose.contrapose₂` `Submodule.ext`
`span_singleton_eq_top` 📖	mathematical	—	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet` `Top.top` `Submodule` `Submodule.instTop`	—	`IsSimpleOrder.eq_bot_or_eq_top` `toIsSimpleOrder` `Eq.le` `Submodule.mem_span_singleton_self`
`toIsSimpleOrder` 📖	mathematical	—	`IsSimpleOrder` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	—
`toSpanSingleton_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.toSpanSingleton`	—	`RingHomSurjective.ids` `LinearMap.range_eq_top` `LinearMap.span_singleton_eq_range` `span_singleton_eq_top`

JordanHolderModule

Definitions

Name	Category	Theorems
`instJordanHolderLattice` 📖	CompOp	2 math math: `isFiniteLength_iff_exists_compositionSeries`, `exists_compositionSeries_of_isNoetherian_isArtinian`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSemisimpleModule_iff` 📖	mathematical	—	`IsSemisimpleModule`	—	`RingHomInvPair.ids` `IsSemisimpleModule.congr`
`isSimpleModule_iff` 📖	mathematical	—	`IsSimpleModule`	—	`RingHomInvPair.ids` `IsSimpleModule.congr`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_ne_zero` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`bijective_or_eq_zero`
`bijective_or_eq_zero` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `instZero`	—	`injective_of_ne_zero` `surjective_of_ne_zero`
`injective_of_ne_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`injective_or_eq_zero`
`injective_or_eq_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `instZero`	—	`ker_eq_bot` `ker_eq_top` `IsSimpleOrder.eq_bot_or_eq_top` `IsSimpleModule.toIsSimpleOrder`
`instIsSimpleModuleEndOfNontrivial` 📖	mathematical	—	`IsSimpleModule` `Module.End` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instRing` `Module.End.applyModule`	—	`isSimpleModule_iff_toSpanSingleton_surjective` `RingHomCompTriple.ids` `IsSemisimpleModule.extension_property` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `ker_eq_bot` `ker_toSpanSingleton` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `one_smul`
`isCoatom_ker_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`IsCoatom` `Submodule` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instOrderTop` `ker`	—	`isSimpleModule_iff_isCoatom` `IsSimpleModule.congr`
`isSemisimpleModule_iff_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`IsSemisimpleModule`	—	`OrderIso.complementedLattice_iff`
`isSimpleModule_iff_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`IsSimpleModule`	—	`OrderIso.isSimpleOrder_iff`
`linearEquiv_of_ne_zero` 📖	mathematical	—	`LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `exists_ne_zero_of_sSup_eq_top` `IsSemisimpleModule.sSup_simples_eq_top` `bijective_or_eq_zero`
`surjective_of_ne_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`surjective_or_eq_zero`
`surjective_or_eq_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `instZero`	—	`RingHomSurjective.ids` `range_eq_top` `range_eq_bot` `IsSimpleOrder.eq_bot_or_eq_top` `IsSimpleModule.toIsSimpleOrder`

Module.End

Definitions

Name	Category	Theorems
`instDivisionRing` 📖	CompOp	—

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule` 📖	mathematical	—	`Module.Finite` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module`	—	`of_isComplemented_domain` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice`
`instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1` 📖	mathematical	—	`Module.Finite` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module` `Submodule.module'` `SetLike.instSMulCommClassSubtypeMem_2` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.smulMemClass`	—	`of_isComplemented_codomain` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice`
`of_isComplemented_codomain` 📖	mathematical	`IsComplemented` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `CompleteLattice.toBoundedOrder`	`Module.Finite` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module` `Submodule.module'` `SetLike.instSMulCommClassSubtypeMem_2` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.smulMemClass`	—	`of_surjective` `SetLike.instSMulCommClassSubtypeMem_2` `Submodule.smulMemClass` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `Submodule.isScalarTower'` `IsScalarTower.left` `LinearMap.surjective_comp_linearProjOfIsCompl`
`of_isComplemented_domain` 📖	mathematical	`IsComplemented` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `CompleteLattice.toBoundedOrder`	`Module.Finite` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module`	—	`of_surjective` `RingHomSurjective.ids` `LinearMap.surjective_comp_subtype_of_isComplemented`
`toModuleEnd_moduleEnd_surjective` 📖	mathematical	—	`Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instSemiring` `Module.End.applyModule` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Module.toModuleEnd` `Module.End.apply_smulCommClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommMonoid.toAddMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction`	—	`Module.End.apply_smulCommClass` `IsScalarTower.left` `fg_top` `jacobson_density` `LinearMap.ext` `Submodule.span_induction` `smul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_add` `map_add` `SemilinearMapClass.toAddHomClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Eq.ge`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSemisimpleRing` 📖	mathematical	—	`IsSemisimpleRing`	—	`RingEquivClass.toRingHomClass` `instRingEquivClass` `RingHomInvPair.of_ringEquiv` `RingHomInvPair.symm` `OrderIso.complementedLattice` `IsSemisimpleModule.toComplementedLattice` `RingHomSurjective.instToRingHomRingEquiv`
`isSemisimpleRing_iff` 📖	mathematical	—	`IsSemisimpleRing`	—	`isSemisimpleRing`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSemisimpleRing_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instFunLike`	`IsSemisimpleRing`	—	`AddMonoidHom.map_add'` `IsSemisimpleRing.eq_1` `LinearMap.isSemisimpleModule_iff_of_bijective` `Function.bijective_id` `IsSemisimpleRing.isSemisimpleModule`

(root)

Definitions

Name	Category	Theorems
`IsSemisimpleModule` 📖	CompData	24 math math: `IsSemisimpleModule.submodule`, `Submodule.isSemisimple_torsionBy_of_irreducible`, `IsSemisimpleModule.of_injective`, `IsSemisimpleModule.sup`, `IsSemisimpleModule.of_sSup_simples_eq_top`, `Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule`, `isSemisimpleModule_iff`, `instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent`, `LinearMap.isSemisimpleModule_iff_of_bijective`, `IsSemisimpleRing.isSemisimpleModule`, `instIsSemisimpleModuleOfIsSimpleModule`, `IsSemisimpleModule.of_surjective`, `Module.IsTorsionBySet.isSemisimpleModule_iff`, `MonoidAlgebra.Submodule.instIsSemisimpleModule`, `instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents`, `LinearEquiv.isSemisimpleModule_iff`, `IsArtinian.isSemisimpleModule_iff_jacobson`, `IsSemisimpleModule.congr`, `sSup_simples_eq_top_iff_isSemisimpleModule`, `IsSemisimpleModule.range`, `IsSemisimpleModule.quotient`, `instIsSemisimpleModuleFinsupp`, `Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule`, `isSemisimpleModule_iff_exists_linearEquiv_dfinsupp`
`IsSemisimpleRing` 📖	MathDef	19 math math: `IsSimpleRing.tfae`, `isSemisimpleRing_iff_pi_matrix_divisionRing`, `IsSimpleRing.isSemisimpleRing_iff_isArtinianRing`, `instIsSemisimpleRingProd`, `IsArtinianRing.isSemisimpleRing_of_isReduced`, `IsSemisimpleRing.moduleEnd`, `IsSemiprimaryRing.isSemisimpleRing`, `IsSemisimpleRing.instMatrix`, `MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebra`, `IsSemisimpleRing.instMulOpposite`, `isSimpleRing_isArtinianRing_iff`, `isSemisimpleRing_mulOpposite_iff`, `RingEquiv.isSemisimpleRing`, `isSemiprimaryRing_iff`, `IsSimpleRing.instIsSemisimpleRing`, `IsArtinianRing.isSemisimpleRing_iff_jacobson`, `RingHom.isSemisimpleRing_of_surjective`, `instIsSemisimpleRingOfSubsingleton`, `RingEquiv.isSemisimpleRing_iff`
`IsSimpleModule` 📖	CompData	42 math math: `IsIsotypic.linearEquiv_fun`, `Representation.IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule`, `covBy_iff_quot_is_simple`, `isSimpleModule_iff_isAtom`, `IsIsotypic.submodule_linearEquiv_fun`, `IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp`, `isSimpleModule_self_iff_isUnit`, `simple_iff_isSimpleModule`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite`, `LinearMap.isSimpleModule_iff_of_bijective`, `Representation.isSimpleModule_iff_irreducible_ofModule`, `RootPairing.isSimpleModule_weylGroupRootRep`, `RootPairing.isSimpleModule_weylGroupRootRep_iff`, `IsSemisimpleModule.sSup_simples_le`, `IsSemisimpleModule.exists_simple_submodule`, `Module.length_eq_one_iff`, `isSimpleModule_iff_quot_maximal`, `IsSemisimpleModule.sSup_simples_eq_top`, `instIsSimpleModule`, `isSimpleModule_iff`, `isSimpleModule_iff_finrank_eq_one`, `IsSemisimpleModule.exists_end_ringEquiv`, `IsSemisimpleModule.exists_end_algEquiv`, `IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite`, `IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end`, `Representation.irreducible_iff_isSimpleModule_asModule`, `IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top`, `instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId`, `isSimpleModule_iff_isCoatom`, `LinearEquiv.isSimpleModule_iff`, `isSimpleModule_iff_toSpanSingleton_surjective`, `IsIsotypic.linearEquiv_finsupp`, `IsSemisimpleModule.eq_bot_or_exists_simple_le`, `Representation.is_simple_module_iff_irreducible_ofModule`, `sSup_simples_eq_top_iff_isSemisimpleModule`, `IsSemisimpleModule.exists_linearEquiv_dfinsupp`, `simple_iff_isSimpleModule'`, `isSimpleModule_of_simple`, `IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end`, `LinearMap.instIsSimpleModuleEndOfNontrivial`, `IsSimpleModule.congr`, `isSemisimpleModule_iff_exists_linearEquiv_dfinsupp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covBy_iff_quot_is_simple` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`CovBy` `Preorder.toLT` `IsSimpleModule` `HasQuotient.Quotient` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Submodule.hasQuotient` `Submodule.addCommGroup` `Submodule.comap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.subtype` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`covBy_iff_coatom_Iic` `isSimpleModule_iff_isCoatom` `OrderIso.isCoatom_iff` `RingHomSurjective.ids` `Submodule.map_comap_subtype` `inf_eq_right`
`instIsPrincipalIdealRingOfIsSemisimpleRing` 📖	mathematical	—	`IsPrincipalIdealRing` `Ring.toSemiring`	—	`IsSemisimpleRing.ideal_eq_span_idempotent`
`instIsSemisimpleModuleDFinsupp` 📖	mathematical	`IsSemisimpleModule`	`DFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFinsupp.addCommGroup` `DFinsupp.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`isSemisimpleModule_of_isSemisimpleModule_submodule'` `RingHomSurjective.ids` `IsSemisimpleModule.range` `DFinsupp.iSup_range_lsingle`
`instIsSemisimpleModuleFinsupp` 📖	mathematical	—	`IsSemisimpleModule` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`isSemisimpleModule_of_isSemisimpleModule_submodule'` `RingHomSurjective.ids` `IsSemisimpleModule.congr` `IsSemisimpleModule.quotient` `RingHomInvPair.ids` `Finsupp.iSup_lsingle_range`
`instIsSemisimpleModuleForallOfFinite` 📖	mathematical	`IsSemisimpleModule`	`Pi.addCommGroup` `Pi.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`isSemisimpleModule_of_isSemisimpleModule_submodule'` `RingHomSurjective.ids` `IsSemisimpleModule.range` `LinearMap.range_eq_map` `Submodule.iSup_map_single` `Submodule.pi_top`
`instIsSemisimpleModuleOfIsSimpleModule` 📖	mathematical	—	`IsSemisimpleModule`	—	`IsSimpleOrder.instComplementedLattice` `IsSimpleModule.toIsSimpleOrder`
`instIsSemisimpleRingForallOfFinite` 📖	mathematical	`IsSemisimpleRing`	`Pi.ring`	—	`AddMonoidHom.map_add'` `LinearMap.isSemisimpleModule_iff_of_bijective` `instRingHomSurjectiveForallEvalRingHom` `Function.bijective_id` `instIsSemisimpleModuleForallOfFinite`
`instIsSemisimpleRingOfSubsingleton` 📖	mathematical	—	`IsSemisimpleRing`	—	`isSemisimpleModule_iff` `Subsingleton.instComplementedLattice` `Unique.instSubsingleton`
`instIsSemisimpleRingProd` 📖	mathematical	—	`IsSemisimpleRing` `Prod.instRing`	—	`AddMonoidHom.map_add'` `IsSemisimpleRing.eq_1` `LinearMap.isSemisimpleModule_iff_of_bijective` `RingHomInvPair.ids` `RingHomSurjective.ids` `LinearEquiv.bijective` `LinearMap.sup_range_inl_inr` `IsSemisimpleModule.sup` `IsSemisimpleModule.range` `RingHom.instRingHomSurjectiveProdFst` `Function.bijective_id` `RingHom.instRingHomSurjectiveProdSnd`
`instIsSimpleModule` 📖	mathematical	—	`IsSimpleModule` `DivisionRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring`	—	`Ideal.isSimpleOrder`
`isSemisimpleModule_biSup_of_isSemisimpleModule_submodule` 📖	mathematical	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership`	—	`isSemisimpleModule_of_isSemisimpleModule_submodule` `LinearEquiv.isSemisimpleModule_iff` `Submodule.injective_subtype` `RingHomSurjective.ids` `Submodule.range_subtype` `le_biSup` `Submodule.biSup_comap_subtype_eq_top`
`isSemisimpleModule_iff` 📖	mathematical	—	`IsSemisimpleModule` `ComplementedLattice` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `CompleteLattice.toBoundedOrder`	—	—
`isSemisimpleModule_iff_exists_linearEquiv_dfinsupp` 📖	mathematical	—	`IsSemisimpleModule` `IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Set` `Set.instMembership` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomInvPair.ids` `IsSemisimpleModule.exists_linearEquiv_dfinsupp` `IsSemisimpleModule.congr` `instIsSemisimpleModuleDFinsupp` `instIsSemisimpleModuleOfIsSimpleModule`
`isSemisimpleModule_of_isSemisimpleModule_submodule` 📖	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership` `Top.top` `Submodule.instTop`	—	—	`complementedLattice_of_complementedLattice_Iic` `Submodule.instIsModularLattice` `Submodule.instIsCompactlyGenerated` `OrderIso.complementedLattice_iff`
`isSemisimpleModule_of_isSemisimpleModule_submodule'` 📖	—	`IsSemisimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Top.top` `Submodule.instTop`	—	—	`isSemisimpleModule_of_isSemisimpleModule_submodule` `iSup_congr_Prop` `iSup_pos`
`isSimpleModule_iff` 📖	mathematical	—	`IsSimpleModule` `IsSimpleOrder` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	—
`isSimpleModule_iff_isAtom` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `IsAtom` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instOrderBot`	—	`Set.isSimpleOrder_Iic_iff_isAtom` `isSimpleModule_iff` `OrderIso.isSimpleOrder_iff`
`isSimpleModule_iff_isCoatom` 📖	mathematical	—	`IsSimpleModule` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `IsCoatom` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.instOrderTop`	—	`Set.isSimpleOrder_Ici_iff_isCoatom` `isSimpleModule_iff` `OrderIso.isSimpleOrder_iff`
`isSimpleModule_iff_quot_maximal` 📖	mathematical	—	`IsSimpleModule` `Ideal.IsMaximal` `Ring.toSemiring` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Ideal` `Submodule.hasQuotient` `Ring.toAddCommGroup` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`RingHomInvPair.ids` `IsSimpleModule.nontrivial` `exists_ne` `IsSimpleModule.ker_toSpanSingleton_isMaximal` `IsSimpleModule.toSpanSingleton_surjective` `IsSimpleModule.congr` `isSimpleModule_iff_isCoatom`
`isSimpleModule_iff_toSpanSingleton_surjective` 📖	mathematical	—	`IsSimpleModule` `Nontrivial` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.toSpanSingleton`	—	`IsSimpleModule.nontrivial` `IsSimpleModule.toSpanSingleton_surjective` `isSimpleModule_iff` `Submodule.instNontrivial` `Submodule.ne_bot_iff` `top_unique` `Submodule.smul_mem`
`isSimpleModule_self_iff_isUnit` 📖	mathematical	—	`IsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Nontrivial` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`isSimpleModule_iff_toSpanSingleton_surjective` `left_ne_zero_of_mul` `one_ne_zero` `NeZero.one` `left_inv_eq_right_inv` `Function.Bijective.surjective` `Units.mulRight_bijective`
`jacobson_density` 📖	mathematical	—	`DFunLike.coe` `Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instSemiring` `Module.End.applyModule` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Finite.of_fintype` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice` `instIsSemisimpleModuleFinsupp` `Submodule.mem_span_singleton_self` `Submodule.IsCompl.projection_apply_left` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Module.End.smul_def` `Submodule.IsCompl.projection_apply_mem` `Submodule.mem_span_singleton`
`sSup_simples_eq_top_iff_isSemisimpleModule` 📖	mathematical	—	`SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `setOf` `IsSimpleModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Top.top` `Submodule.instTop` `IsSemisimpleModule`	—	`IsSemisimpleModule.of_sSup_simples_eq_top` `IsSemisimpleModule.sSup_simples_eq_top`

---

← Back to Index