InjectiveProjective

Statistics

Metric	Count
Definitions	0
Theorems `injective_of_isSemisimpleRing`, `injective_of_semisimple_ring`, `projective_of_isSemisimpleRing`, `projective_of_semisimple_ring`	4
Total	4

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

---