Simple

📁 Source: Mathlib/Algebra/Category/ModuleCat/Simple.lean

Statistics

Metric	Count
Definitions	0
Theorems isSimpleModule_of_simple, simple_iff_isSimpleModule, simple_iff_isSimpleModule', simple_of_finrank_eq_one, simple_of_isSimpleModule	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSimpleModule_of_simple 📖	mathematical	—	IsSimpleModule ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule	—	simple_iff_isSimpleModule
simple_iff_isSimpleModule 📖	mathematical	—	CategoryTheory.Simple ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.of IsSimpleModule	—	CategoryTheory.Limits.HasZeroObject.hasInitial ModuleCat.instHasZeroObject CategoryTheory.Limits.HasZeroObject.initialMonoClass CategoryTheory.simple_iff_subobject_isSimpleOrder OrderIso.isSimpleOrder_iff isSimpleModule_iff
simple_iff_isSimpleModule' 📖	mathematical	—	CategoryTheory.Simple ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive IsSimpleModule ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule	—	simple_iff_isSimpleModule
simple_of_finrank_eq_one 📖	mathematical	Module.finrank ModuleCat.carrier DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.moduleOfAlgebraModule	CategoryTheory.Simple ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	—	simple_iff_isSimpleModule' isSimpleModule_iff is_simple_module_of_finrank_eq_one ModuleCat.isScalarTower_of_algebra_moduleCat
simple_of_isSimpleModule 📖	mathematical	—	CategoryTheory.Simple ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.of	—	simple_iff_isSimpleModule

---

← Back to Index