GrpWithZero

📁 Source: Mathlib/Algebra/Category/GrpWithZero.lean

Statistics

Metric	Count
Definitions GrpWithZero, mk, carrier, groupWithZeroConcreteCategory, hasForgetToBipointed, hasForgetToMon, instCoeSortType, instInhabited, instLargeCategory, ofHom, str	11
Theorems mk_hom, mk_inv, coe_comp, coe_id, forget_map, hom_comp, hom_id	7
Total	18

GrpWithZero

Definitions

Name	Category	Theorems
carrier 📖	CompOp	7 math math: forget_map, hom_comp, coe_id, coe_comp, Iso.mk_hom, hom_id, Iso.mk_inv
groupWithZeroConcreteCategory 📖	CompOp	5 math math: forget_map, hom_comp, coe_id, coe_comp, hom_id
hasForgetToBipointed 📖	CompOp	—
hasForgetToMon 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	7 math math: forget_map, hom_comp, coe_id, coe_comp, Iso.mk_hom, hom_id, Iso.mk_inv
ofHom 📖	CompOp	2 math math: Iso.mk_hom, Iso.mk_inv
str 📖	CompOp	7 math math: forget_map, hom_comp, coe_id, coe_comp, Iso.mk_hom, hom_id, Iso.mk_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom GrpWithZero instLargeCategory MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero str MonoidWithZeroHom.funLike groupWithZeroConcreteCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom GrpWithZero instLargeCategory MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero str MonoidWithZeroHom.funLike groupWithZeroConcreteCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map GrpWithZero instLargeCategory CategoryTheory.types CategoryTheory.forget MonoidWithZeroHom carrier MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero str MonoidWithZeroHom.funLike groupWithZeroConcreteCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom GrpWithZero instLargeCategory MonoidWithZeroHom carrier MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero str MonoidWithZeroHom.funLike groupWithZeroConcreteCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct MonoidWithZeroHom.comp	—	—
hom_id 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom GrpWithZero instLargeCategory MonoidWithZeroHom carrier MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero str MonoidWithZeroHom.funLike groupWithZeroConcreteCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct MonoidWithZeroHom.id	—	—

GrpWithZero.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom GrpWithZero GrpWithZero.instLargeCategory GrpWithZero.ofHom GrpWithZero.carrier GrpWithZero.str MonoidWithZeroHomClass.toMonoidWithZeroHom MulEquiv MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero EquivLike.toFunLike MulEquiv.instEquivLike	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv GrpWithZero GrpWithZero.instLargeCategory GrpWithZero.ofHom GrpWithZero.carrier GrpWithZero.str MonoidWithZeroHomClass.toMonoidWithZeroHom MulEquiv MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm	—	—

(root)

Definitions

Name	Category	Theorems
GrpWithZero 📖	CompData	7 math math: GrpWithZero.forget_map, GrpWithZero.hom_comp, GrpWithZero.coe_id, GrpWithZero.coe_comp, GrpWithZero.Iso.mk_hom, GrpWithZero.hom_id, GrpWithZero.Iso.mk_inv

---

← Back to Index