HasExt

📁 Source: Mathlib/Algebra/Category/ModuleCat/Ext/HasExt.lean

Statistics

Metric	Count
Definitions	0
Theorems instHasExtModuleCatOfSmall	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasExtModuleCatOfSmall 📖	mathematical	—	CategoryTheory.HasExt ModuleCat ModuleCat.moduleCategory ModuleCat.abelian	—	CategoryTheory.hasExt_of_enoughProjectives CategoryTheory.locallySmall_of_univLE UnivLE.self ModuleCat.enoughProjectives

---

← Back to Index