Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/PresentedMonoid/Basic.lean

Statistics

Metric	Count
Definitions `PresentedAddMonoid`, `instAddMonoid`, `mk`, `of`, `PresentedMonoid`, `instMonoid`, `mk`, `of`	8
Theorems `closure_range_of`, `ext`, `ext_iff`, `inductionOn`, `inductionOn₂`, `inductionOn₃`, `lift_of`, `surjective_mk`, `unique`, `closure_range_of`, `ext`, `ext_iff`, `inductionOn`, `inductionOn₂`, `inductionOn₃`, `lift_of`, `surjective_mk`, `unique`	18
Total	26

PresentedAddMonoid

Definitions

Name	Category	Theorems
`instAddMonoid` 📖	CompOp	4 math math: `ext_iff`, `surjective_mk`, `lift_of`, `closure_range_of`
`mk` 📖	CompOp	—
`of` 📖	CompOp	3 math math: `ext_iff`, `lift_of`, `closure_range_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_range_of` 📖	mathematical	—	`AddSubmonoid.closure` `PresentedAddMonoid` `AddMonoid.toAddZeroClass` `instAddMonoid` `Set.range` `of` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	—	`AddSubmonoid.eq_top_iff'` `inductionOn` `FreeAddMonoid.inductionOn` `AddSubmonoid.zero_mem` `AddSubmonoid.subset_closure` `AddSubmonoid.add_mem`
`ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `PresentedAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `of`	—	—	`AddMonoidHom.eq_of_eqOn_denseM` `closure_range_of`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `PresentedAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `of`	—	`ext`
`inductionOn` 📖	—	`DFunLike.coe` `AddMonoidHom` `FreeAddMonoid` `PresentedAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `instAddMonoid` `AddMonoidHom.instFunLike`	—	—	—
`inductionOn₂` 📖	—	`DFunLike.coe` `AddMonoidHom` `FreeAddMonoid` `PresentedAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `instAddMonoid` `AddMonoidHom.instFunLike`	—	—	—
`inductionOn₃` 📖	—	`DFunLike.coe` `AddMonoidHom` `FreeAddMonoid` `PresentedAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `instAddMonoid` `AddMonoidHom.instFunLike`	—	—	—
`lift_of` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `FreeAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAddMonoid.lift`	`PresentedAddMonoid` `instAddMonoid` `lift` `of`	—	—
`surjective_mk` 📖	mathematical	—	`FreeAddMonoid` `PresentedAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `instAddMonoid` `AddMonoidHom.instFunLike`	—	`inductionOn`

PresentedAddMonoid.toMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unique` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `FreeAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeAddMonoid.lift` `AddCon.Quotient` `AddZero.toAdd` `addConGen` `AddCon.addZeroClass` `PresentedAddMonoid.of`	`PresentedAddMonoid.lift`	—	`AddCon.lift_unique` `AddCon.addConGen_le` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `FreeAddMonoid.hom_eq`

PresentedMonoid

Definitions

Name	Category	Theorems
`instMonoid` 📖	CompOp	4 math math: `closure_range_of`, `lift_of`, `surjective_mk`, `ext_iff`
`mk` 📖	CompOp	—
`of` 📖	CompOp	3 math math: `closure_range_of`, `lift_of`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_range_of` 📖	mathematical	—	`Submonoid.closure` `PresentedMonoid` `Monoid.toMulOneClass` `instMonoid` `Set.range` `of` `Top.top` `Submonoid` `Submonoid.instTop`	—	`Submonoid.eq_top_iff'` `inductionOn` `FreeMonoid.inductionOn` `Submonoid.one_mem` `Submonoid.subset_closure` `Submonoid.mul_mem`
`ext` 📖	—	`DFunLike.coe` `MonoidHom` `PresentedMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MonoidHom.instFunLike` `of`	—	—	`MonoidHom.eq_of_eqOn_denseM` `closure_range_of`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `PresentedMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `MonoidHom.instFunLike` `of`	—	`ext`
`inductionOn` 📖	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `PresentedMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `instMonoid` `MonoidHom.instFunLike`	—	—	—
`inductionOn₂` 📖	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `PresentedMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `instMonoid` `MonoidHom.instFunLike`	—	—	—
`inductionOn₃` 📖	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `PresentedMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `instMonoid` `MonoidHom.instFunLike`	—	—	—
`lift_of` 📖	mathematical	`DFunLike.coe` `MonoidHom` `FreeMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.lift`	`PresentedMonoid` `instMonoid` `lift` `of`	—	—
`surjective_mk` 📖	mathematical	—	`FreeMonoid` `PresentedMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `instMonoid` `MonoidHom.instFunLike`	—	`inductionOn`

PresentedMonoid.toMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unique` 📖	mathematical	`DFunLike.coe` `MonoidHom` `FreeMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.lift` `Con.Quotient` `MulOne.toMul` `conGen` `Con.mulOneClass` `PresentedMonoid.of`	`PresentedMonoid.lift`	—	`Con.lift_unique` `Con.conGen_le` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `FreeMonoid.hom_eq`

(root)

Definitions

Name	Category	Theorems
`PresentedAddMonoid` 📖	CompOp	4 math math: `PresentedAddMonoid.ext_iff`, `PresentedAddMonoid.surjective_mk`, `PresentedAddMonoid.lift_of`, `PresentedAddMonoid.closure_range_of`
`PresentedMonoid` 📖	CompOp	4 math math: `PresentedMonoid.closure_range_of`, `PresentedMonoid.lift_of`, `PresentedMonoid.surjective_mk`, `PresentedMonoid.ext_iff`

---

← Back to Index