Semisimple

📁 Source: Mathlib/RepresentationTheory/Semisimple.lean

Statistics

Metric	Count
Definitions IsSemisimpleRepresentation	1
Theorems isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule, isSemisimpleRepresentation_iff_isSemisimpleModule_asModule	2
Total	3

Representation

Definitions

Name	Category	Theorems
IsSemisimpleRepresentation 📖	MathDef	3 math math: MonoidAlgebra.Submodule.instIsSemisimpleRepresentation, isSemisimpleRepresentation_iff_isSemisimpleModule_asModule, isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule 📖	mathematical	—	IsSemisimpleModule MonoidAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidAlgebra.ring DivisionRing.toRing Field.toDivisionRing IsSemisimpleRepresentation RestrictScalars CommSemiring.toSemiring Semifield.toCommSemiring RestrictScalars.module MonoidAlgebra.semiring AddCommGroup.toAddCommMonoid MonoidAlgebra.algebra Algebra.id ofModule	—	isSemisimpleModule_iff OrderIso.complementedLattice_iff
isSemisimpleRepresentation_iff_isSemisimpleModule_asModule 📖	mathematical	—	IsSemisimpleRepresentation IsSemisimpleModule MonoidAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidAlgebra.ring DivisionRing.toRing Field.toDivisionRing asModule Semifield.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupAsModule EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleMonoidAlgebraAsModule	—	isSemisimpleModule_iff OrderIso.complementedLattice_iff

---

← Back to Index