LargeColimits

Statistics

Metric	Count
Definitions	0
Theorems `hasColimit_iff_small_quot`, `isColimit_iff_bijective_desc`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit_iff_small_quot` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `AddCommGrpCat` `instCategory` `Small` `Colimits.Quot`	—	`isColimit_iff_bijective_desc` `hasColimit_of_small_quot`
`isColimit_iff_bijective_desc` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit` `AddCommGrpCat` `instCategory` `Function.Bijective` `Colimits.Quot` `carrier` `CategoryTheory.Limits.Cocone.pt` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Colimits.instAddCommGroupQuot` `str` `AddMonoidHom.instFunLike` `Colimits.Quot.desc`	—	`CharacterModule.dual_bijective_iff_bijective` `Equiv.injective` `AddSubgroup.normal_of_comm` `ofHom_injective` `CategoryTheory.Limits.IsColimit.hom_ext` `hom_ext` `AddMonoidHom.ext` `ULift.ext` `CategoryTheory.ConcreteCategory.comp_apply` `Colimits.Quot.ι_desc` `DFunLike.congr_fun` `Colimits.Quot.map_ι` `Colimits.Quot.addMonoidHom_ext` `CategoryTheory.Limits.IsColimit.fac` `AddEquiv.apply_symm_apply`

---