Documentation Verification Report

FiniteGrp

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

Statistics

Metric	Count
Definitions `FiniteAddGrp`, `instAddGroupCarrierToAddGrp`, `instCategory`, `instCoeSortType`, `instConcreteCategoryAddMonoidHomCarrierToAddGrp`, `of`, `ofHom`, `toAddGrp`, `FiniteGrp`, `instCategory`, `instCoeSortType`, `instConcreteCategoryMonoidHomCarrierToGrp`, `instGroupCarrierToGrp`, `of`, `ofHom`, `toGrp`	16
Theorems `instFiniteCarrierToAddGrp`, `isFinite`, `ofHom_apply`, `instFiniteCarrierToGrp`, `isFinite`, `ofHom_apply`	6
Total	22

FiniteAddGrp

Definitions

Name	Category	Theorems
`instAddGroupCarrierToAddGrp` 📖	CompOp	—
`instCategory` 📖	CompOp	1 math math: `ofHom_apply`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryAddMonoidHomCarrierToAddGrp` 📖	CompOp	1 math math: `ofHom_apply`
`of` 📖	CompOp	1 math math: `ofHom_apply`
`ofHom` 📖	CompOp	1 math math: `ofHom_apply`
`toAddGrp` 📖	CompOp	3 math math: `instFiniteCarrierToAddGrp`, `ofHom_apply`, `isFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteCarrierToAddGrp` 📖	mathematical	—	`Finite` `AddGrpCat.carrier` `toAddGrp`	—	`isFinite`
`isFinite` 📖	mathematical	—	`Finite` `AddGrpCat.carrier` `toAddGrp`	—	—
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `CategoryTheory.ConcreteCategory.hom` `FiniteAddGrp` `instCategory` `AddMonoidHom` `AddGrpCat.carrier` `toAddGrp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddGrpCat.str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrierToAddGrp` `ofHom`	—	—

FiniteGrp

Definitions

Name	Category	Theorems
`instCategory` 📖	CompOp	6 math math: `finGaloisGroupMap.map_id`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `ofHom_apply`, `ProfiniteGrp.diagram_map`, `finGaloisGroupMap.map_comp`, `ProfiniteGrp.diagram_obj`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryMonoidHomCarrierToGrp` 📖	CompOp	4 math math: `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `ofHom_apply`, `ProfiniteGrp.diagram_map`, `ProfiniteGrp.diagram_obj`
`instGroupCarrierToGrp` 📖	CompOp	—
`of` 📖	CompOp	1 math math: `ofHom_apply`
`ofHom` 📖	CompOp	1 math math: `ofHom_apply`
`toGrp` 📖	CompOp	6 math math: `isFinite`, `instFiniteCarrierToGrp`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `ofHom_apply`, `ProfiniteGrp.diagram_map`, `ProfiniteGrp.diagram_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteCarrierToGrp` 📖	mathematical	—	`Finite` `GrpCat.carrier` `toGrp`	—	`isFinite`
`isFinite` 📖	mathematical	—	`Finite` `GrpCat.carrier` `toGrp`	—	—
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `CategoryTheory.ConcreteCategory.hom` `FiniteGrp` `instCategory` `MonoidHom` `GrpCat.carrier` `toGrp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrierToGrp` `ofHom`	—	—

(root)

Definitions

Name	Category	Theorems
`FiniteAddGrp` 📖	CompData	1 math math: `FiniteAddGrp.ofHom_apply`
`FiniteGrp` 📖	CompData	6 math math: `finGaloisGroupMap.map_id`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `FiniteGrp.ofHom_apply`, `ProfiniteGrp.diagram_map`, `finGaloisGroupMap.map_comp`, `ProfiniteGrp.diagram_obj`

---

← Back to Index