Subobject

📁 Source: Mathlib/Algebra/Category/Grp/Subobject.lean

Statistics

Metric	Count
Definitions	0
Theorems wellPowered_addCommGrp	1
Total	1

AddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
wellPowered_addCommGrp 📖	mathematical	—	CategoryTheory.WellPowered AddCommGrpCat instCategory CategoryTheory.locallySmall_of_univLE UnivLE.self	—	CategoryTheory.wellPowered_of_equiv ModuleCat.forget₂AddCommGroupIsEquivalence CategoryTheory.locallySmall_of_univLE UnivLE.self ModuleCat.wellPowered_moduleCat

---

← Back to Index