InjectiveProjective

Statistics

Metric	Count
Definitions	0
Theorems `injective_of_isSemisimpleRing`, `projective_of_isSemisimpleRing`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_of_isSemisimpleRing` 📖	mathematical	—	`Injective`	—	`RingHomCompTriple.ids` `IsSemisimpleModule.extension_property` `IsSemisimpleRing.isSemisimpleModule` `LinearMap.comp_apply`
`projective_of_isSemisimpleRing` 📖	mathematical	—	`Projective` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Projective.of_lifting_property''` `IsSemisimpleModule.lifting_property` `instIsSemisimpleModuleFinsupp`

---