Documentation Verification Report

GrothendieckGroup

📁 Source: Mathlib/GroupTheory/MonoidLocalization/GrothendieckGroup.lean

Statistics

Metric	Count
Definitions `GrothendieckAddGroup`, `instAddCommGroup`, `instNeg`, `of`, `GrothendieckGroup`, `instCommGroup`, `instInv`, `of`	8
Theorems `lift_apply`, `lift_symm_apply`, `mk_sub_mk`, `neg_mk`, `of_injective`, `inv_mk`, `lift_apply`, `lift_symm_apply`, `mk_div_mk`, `of_injective`	10
Total	18

Algebra

Definitions

Name	Category	Theorems
`GrothendieckAddGroup` 📖	CompOp	4 math math: `GrothendieckAddGroup.instFG`, `GrothendieckAddGroup.of_injective`, `GrothendieckAddGroup.lift_apply`, `GrothendieckAddGroup.lift_symm_apply`
`GrothendieckGroup` 📖	CompOp	4 math math: `GrothendieckGroup.instFG`, `GrothendieckGroup.lift_symm_apply`, `GrothendieckGroup.lift_apply`, `GrothendieckGroup.of_injective`

Algebra.GrothendieckAddGroup

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	1 math math: `mk_sub_mk`
`instNeg` 📖	CompOp	1 math math: `neg_mk`
`of` 📖	CompOp	2 math math: `of_injective`, `lift_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Algebra.GrothendieckAddGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddOreLocalization.instAddMonoid` `AddCommMonoid.toAddMonoid` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop` `AddOreLocalization.addOreSetComm` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `SubNegMonoid.toSub` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.LocalizationMap.sec` `AddLocalization` `AddOreLocalization.instAddCommMonoid` `AddLocalization.addMonoidOf`	—	`AddSubmonoid.instAddSubmonoidClass` `AddSubmonoid.LocalizationMap.lift_apply` `AddUnits.val_neg_eq_neg_val` `sub_eq_add_neg` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `Algebra.GrothendieckAddGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddOreLocalization.instAddMonoid` `AddCommMonoid.toAddMonoid` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop` `AddOreLocalization.addOreSetComm` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AddMonoidHom.comp` `of`	—	—
`mk_sub_mk` 📖	mathematical	—	`AddLocalization` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.instTop` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.mem_top`	—	`AddSubmonoid.mem_top` `sub_eq_add_neg` `AddLocalization.mk_add`
`neg_mk` 📖	mathematical	—	`AddLocalization` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.instTop` `instNeg` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.mem_top`	—	—
`of_injective` 📖	mathematical	—	`Algebra.GrothendieckAddGroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddOreLocalization.instAddMonoid` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop` `AddOreLocalization.addOreSetComm` `AddMonoidHom.instFunLike` `of`	—	`AddLocalization.mk_eq_mk_iff'` `zero_add`

Algebra.GrothendieckGroup

Definitions

Name	Category	Theorems
`instCommGroup` 📖	CompOp	1 math math: `mk_div_mk`
`instInv` 📖	CompOp	1 math math: `inv_mk`
`of` 📖	CompOp	2 math math: `lift_symm_apply`, `of_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_mk` 📖	mathematical	—	`Localization` `Top.top` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid.instTop` `instInv` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.mem_top`	—	—
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Algebra.GrothendieckGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `OreLocalization.instMonoid` `CommMonoid.toMonoid` `Top.top` `Submonoid` `Submonoid.instTop` `OreLocalization.oreSetComm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `DivInvMonoid.toDiv` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.LocalizationMap.sec` `Localization` `OreLocalization.instCommMonoid` `Localization.monoidOf`	—	`Submonoid.instSubmonoidClass` `Submonoid.LocalizationMap.lift_apply` `Units.val_inv_eq_inv_val` `div_eq_mul_inv` `LeftCancelSemigroup.toIsLeftCancelMul`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Algebra.GrothendieckGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `OreLocalization.instMonoid` `CommMonoid.toMonoid` `Top.top` `Submonoid` `Submonoid.instTop` `OreLocalization.oreSetComm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.comp` `of`	—	—
`mk_div_mk` 📖	mathematical	—	`Localization` `Top.top` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid.instTop` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `MulOne.toMul` `MulOneClass.toMulOne` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.mem_top`	—	`Submonoid.mem_top` `div_eq_mul_inv` `Localization.mk_mul`
`of_injective` 📖	mathematical	—	`Algebra.GrothendieckGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OreLocalization.instMonoid` `Top.top` `Submonoid` `Submonoid.instTop` `OreLocalization.oreSetComm` `MonoidHom.instFunLike` `of`	—	`one_mul`

---

← Back to Index