Documentation Verification Report

DivPairs

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

Statistics

Metric	Count
Definitions `subPairs`, `divPairs`	2
Theorems `mem_subPairs`, `subPairs_comap`, `divPairs_comap`, `mem_divPairs`	4
Total	6

AddSubmonoid

Definitions

Name	Category	Theorems
`subPairs` 📖	CompOp	2 math math: `subPairs_comap`, `mem_subPairs`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_subPairs` 📖	mathematical	—	`AddSubmonoid` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `subPairs` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `DFunLike.coe` `LocalizationMap` `Top.top` `instTop` `AddCommGroup.toAddCommMonoid` `LocalizationMap.instFunLike`	—	—
`subPairs_comap` 📖	mathematical	—	`subPairs` `comap` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom` `LocalizationMap.addEquivOfLocalizations` `Top.top` `AddSubmonoid` `AddCommMonoid.toAddMonoid` `instTop` `AddCommGroup.toAddCommMonoid`	—	`ext` `AddMonoidHom.instAddMonoidHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `mem_subPairs` `mem_comap` `LocalizationMap.map_addUnits` `map_sub` `LocalizationMap.lift_eq`

Submonoid

Definitions

Name	Category	Theorems
`divPairs` 📖	CompOp	2 math math: `mem_divPairs`, `divPairs_comap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divPairs_comap` 📖	mathematical	—	`divPairs` `comap` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom` `LocalizationMap.mulEquivOfLocalizations` `Top.top` `Submonoid` `CommMonoid.toMonoid` `instTop` `CommGroup.toCommMonoid`	—	`ext` `MonoidHom.instMonoidHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `LocalizationMap.map_units` `map_div` `LocalizationMap.lift_eq`
`mem_divPairs` 📖	mathematical	—	`Submonoid` `Prod.instMulOneClass` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `divPairs` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivInvMonoid.toDiv` `DFunLike.coe` `LocalizationMap` `Top.top` `instTop` `CommGroup.toCommMonoid` `LocalizationMap.instFunLike`	—	—

---

← Back to Index