EnoughInjectives

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

Statistics

Metric	Count
Definitions	0
Theorems enoughInjectives, instEnoughInjectivesModuleCatInt, instEnoughInjectivesModuleCatOfSmall	3
Total	3

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughInjectives 📖	mathematical	—	CategoryTheory.EnoughInjectives ModuleCat moduleCategory	—	CategoryTheory.EnoughInjectives.of_adjunction instPreservesMonomorphismsRestrictScalars CategoryTheory.Functor.reflectsMonomorphisms_of_faithful instFaithfulRestrictScalars instEnoughInjectivesModuleCatInt

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEnoughInjectivesModuleCatInt 📖	mathematical	—	CategoryTheory.EnoughInjectives ModuleCat Int.instRing ModuleCat.moduleCategory	—	CategoryTheory.EnoughInjectives.of_equivalence ModuleCat.forget₂AddCommGroupIsEquivalence AddCommGrpCat.enoughInjectives
instEnoughInjectivesModuleCatOfSmall 📖	mathematical	—	CategoryTheory.EnoughInjectives ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.EnoughInjectives.of_equivalence ModuleCat.restrictScalars_isEquivalence_of_ringEquiv ModuleCat.enoughInjectives

---

← Back to Index