EnoughInjectives

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

Statistics

Metric	Count
Definitions	0
Theorems enoughInjectives, enoughInjectives	2
Total	2

AddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughInjectives 📖	mathematical	—	CategoryTheory.EnoughInjectives AddCommGrpCat instCategory	—	injective_of_divisible AddSubgroup.normal_of_comm Rat.instIsStrictOrderedRing ZeroLEOneClass.factZeroLtOne Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass CharacterModule.instLinearMapClassIntAddCircleRatOfNat map_add SemilinearMapClass.toAddHomClass mono_iff_injective injective_iff_map_eq_zero AddMonoidHom.instAddMonoidHomClass CharacterModule.eq_zero_of_character_apply

CommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enoughInjectives 📖	mathematical	—	CategoryTheory.EnoughInjectives CommGrpCat instCategory	—	CategoryTheory.EnoughInjectives.of_equivalence CategoryTheory.Equivalence.isEquivalence_functor AddCommGrpCat.enoughInjectives

---

← Back to Index