Zero

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

Statistics

Metric	Count
Definitions	0
Theorems hasZeroObject, isZero_iff_subsingleton, isZero_of_subsingleton, subsingleton_of_isZero, hasZeroObject, isZero_iff_subsingleton, isZero_of_subsingleton, subsingleton_of_isZero, instHasZeroObject, isZero_iff_subsingleton, isZero_of_subsingleton, subsingleton_of_isZero, instHasZeroObject, isZero_iff_subsingleton, isZero_of_subsingleton, subsingleton_of_isZero	16
Total	16

AddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject AddCommGrpCat instCategory	—	isZero_of_subsingleton
isZero_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero AddCommGrpCat instCategory carrier	—	subsingleton_of_isZero isZero_of_subsingleton
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero AddCommGrpCat instCategory	—	hom_ext AddMonoidHom.ext map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero AddCommGrpCat instCategory	carrier	—	Equiv.subsingleton isZero_of_subsingleton

AddGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject AddGrpCat instCategory	—	isZero_of_subsingleton
isZero_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero AddGrpCat instCategory carrier	—	subsingleton_of_isZero isZero_of_subsingleton
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero AddGrpCat instCategory	—	hom_ext AddMonoidHom.ext map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero AddGrpCat instCategory	carrier	—	Equiv.subsingleton isZero_of_subsingleton

CommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject CommGrpCat instCategory	—	isZero_of_subsingleton
isZero_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero CommGrpCat instCategory carrier	—	subsingleton_of_isZero isZero_of_subsingleton
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero CommGrpCat instCategory	—	hom_ext MonoidHom.ext map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero CommGrpCat instCategory	carrier	—	Equiv.subsingleton isZero_of_subsingleton

GrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject GrpCat instCategory	—	isZero_of_subsingleton
isZero_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero GrpCat instCategory carrier	—	subsingleton_of_isZero isZero_of_subsingleton
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero GrpCat instCategory	—	hom_ext MonoidHom.ext map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero GrpCat instCategory	carrier	—	Equiv.subsingleton isZero_of_subsingleton

---

← Back to Index