Documentation Verification Report

Graph

📁 Source: Mathlib/Algebra/Group/Graph.lean

Statistics

Metric	Count
Definitions `graph`, `mgraph`, `graph`, `mgraph`	4
Theorems `coe_graph`, `coe_mgraph`, `exists_addEquiv_mrange_eq_mgraph`, `exists_addEquiv_range_eq_graph`, `exists_mrange_eq_mgraph`, `exists_range_eq_graph`, `graph_eq_range_prod`, `graph_toAddSubmonoid`, `mem_graph`, `mem_mgraph`, `mgraph_eq_mrange_prod`, `exists_addEquiv_eq_graph`, `exists_eq_graph`, `exists_addEquiv_eq_mgraph`, `exists_eq_mgraph`, `coe_graph`, `coe_mgraph`, `exists_mrange_eq_mgraph`, `exists_mulEquiv_mrange_eq_mgraph`, `exists_mulEquiv_range_eq_graph`, `exists_range_eq_graph`, `graph_eq_range_prod`, `graph_toSubmonoid`, `mem_graph`, `mem_mgraph`, `mgraph_eq_mrange_prod`, `exists_eq_graph`, `exists_mulEquiv_eq_graph`, `exists_eq_mgraph`, `exists_mulEquiv_eq_mgraph`	30
Total	34

AddMonoidHom

Definitions

Name	Category	Theorems
`graph` 📖	CompOp	10 math math: `exists_range_eq_graph`, `mem_graph`, `AddSubgroup.exists_eq_graph`, `coe_graph`, `graph_toAddSubmonoid`, `graph_eq_range_prod`, `AddSubgroup.goursat_surjective`, `AddSubgroup.exists_addEquiv_eq_graph`, `exists_addEquiv_range_eq_graph`, `AddSubgroup.goursat`
`mgraph` 📖	CompOp	8 math math: `mgraph_eq_mrange_prod`, `AddSubmonoid.exists_eq_mgraph`, `graph_toAddSubmonoid`, `coe_mgraph`, `exists_addEquiv_mrange_eq_mgraph`, `AddSubmonoid.exists_addEquiv_eq_mgraph`, `mem_mgraph`, `exists_mrange_eq_mgraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_graph` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `Prod.instAddGroup` `AddSubgroup.instSetLike` `graph` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	—	—
`coe_mgraph` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike` `mgraph` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike`	—	—
`exists_addEquiv_mrange_eq_mgraph` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike`	`mrange` `instAddMonoidHomClass` `mgraph` `AddEquiv.toAddMonoidHom`	—	`instAddMonoidHomClass` `exists_mrange_eq_mgraph` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `mem_mrange` `Prod.swap_eq_iff_eq_swap` `mem_mgraph` `SetLike.ext_iff` `map_add'`
`exists_addEquiv_range_eq_graph` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Prod.instAddZeroClass` `instFunLike`	`range` `Prod.instAddGroup` `graph` `AddEquiv.toAddMonoidHom`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `SetLike.ext_iff` `mem_range` `instAddMonoidHomClass` `mem_mrange` `mem_mgraph` `exists_addEquiv_mrange_eq_mgraph`
`exists_mrange_eq_mgraph` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike`	`mrange` `instAddMonoidHomClass` `mgraph`	—	`instAddMonoidHomClass` `Set.exists_range_eq_graphOn_univ` `Set.ext_iff` `Set.mem_range` `Set.mem_graphOn` `Set.mem_univ` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Function.Surjective.forall` `map_add` `AddMonoidHomClass.toAddHomClass` `SetLike.ext_iff` `mem_mrange` `mem_mgraph`
`exists_range_eq_graph` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Prod.instAddZeroClass` `instFunLike`	`range` `Prod.instAddGroup` `graph`	—	`SetLike.ext_iff` `mem_range` `instAddMonoidHomClass` `mem_mrange` `mem_mgraph` `exists_mrange_eq_mgraph`
`graph_eq_range_prod` 📖	mathematical	—	`graph` `range` `Prod.instAddGroup` `prod` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `id` `AddZeroClass.toAddZero`	—	`AddSubgroup.ext` `mem_range`
`graph_toAddSubmonoid` 📖	mathematical	—	`AddSubgroup.toAddSubmonoid` `Prod.instAddGroup` `graph` `mgraph` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`mem_graph` 📖	mathematical	—	`AddSubgroup` `Prod.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `graph` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	—	—
`mem_mgraph` 📖	mathematical	—	`AddSubmonoid` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `mgraph` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike`	—	—
`mgraph_eq_mrange_prod` 📖	mathematical	—	`mgraph` `mrange` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `instAddMonoidHomClass` `prod` `id`	—	`AddSubmonoid.ext` `instAddMonoidHomClass` `mem_mgraph` `mem_mrange`

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_addEquiv_eq_graph` 📖	mathematical	`Function.Bijective` `AddSubgroup` `Prod.instAddGroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddMonoidHom.instFunLike` `subtype`	`AddMonoidHom.graph` `AddEquiv.toAddMonoidHom`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `SetLike.ext_iff` `mem_toAddSubmonoid` `AddMonoidHom.mem_mgraph` `AddSubmonoid.exists_addEquiv_eq_mgraph`
`exists_eq_graph` 📖	mathematical	`Function.Bijective` `AddSubgroup` `Prod.instAddGroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup` `AddMonoidHom.instFunLike` `subtype`	`AddMonoidHom.graph`	—	`SetLike.ext_iff` `mem_toAddSubmonoid` `AddMonoidHom.mem_mgraph` `AddSubmonoid.exists_eq_mgraph`

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_addEquiv_eq_mgraph` 📖	mathematical	`Function.Bijective` `AddSubmonoid` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `toAddZeroClass` `AddMonoidHom.instFunLike` `subtype`	`AddMonoidHom.mgraph` `AddEquiv.toAddMonoidHom`	—	`AddMonoidHom.instAddMonoidHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `mrange_subtype` `AddMonoidHom.exists_addEquiv_mrange_eq_mgraph` `Function.Bijective.surjective` `Function.Bijective.injective`
`exists_eq_mgraph` 📖	mathematical	`Function.Bijective` `AddSubmonoid` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `toAddZeroClass` `AddMonoidHom.instFunLike` `subtype`	`AddMonoidHom.mgraph`	—	`AddMonoidHom.instAddMonoidHomClass` `mrange_subtype` `AddMonoidHom.exists_mrange_eq_mgraph` `Function.Bijective.surjective` `Function.Bijective.injective`

MonoidHom

Definitions

Name	Category	Theorems
`graph` 📖	CompOp	10 math math: `graph_eq_range_prod`, `Subgroup.exists_mulEquiv_eq_graph`, `graph_toSubmonoid`, `coe_graph`, `exists_range_eq_graph`, `Subgroup.goursat_surjective`, `mem_graph`, `exists_mulEquiv_range_eq_graph`, `Subgroup.goursat`, `Subgroup.exists_eq_graph`
`mgraph` 📖	CompOp	8 math math: `Submonoid.exists_eq_mgraph`, `graph_toSubmonoid`, `mgraph_eq_mrange_prod`, `coe_mgraph`, `Submonoid.exists_mulEquiv_eq_mgraph`, `exists_mrange_eq_mgraph`, `exists_mulEquiv_mrange_eq_mgraph`, `mem_mgraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_graph` 📖	mathematical	—	`SetLike.coe` `Subgroup` `Prod.instGroup` `Subgroup.instSetLike` `graph` `setOf` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike`	—	—
`coe_mgraph` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Prod.instMulOneClass` `Monoid.toMulOneClass` `Submonoid.instSetLike` `mgraph` `setOf` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instFunLike`	—	—
`exists_mrange_eq_mgraph` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike`	`mrange` `instMonoidHomClass` `mgraph`	—	`instMonoidHomClass` `Set.exists_range_eq_graphOn_univ` `map_one` `MonoidHomClass.toOneHomClass` `Function.Surjective.forall` `map_mul` `MonoidHomClass.toMulHomClass`
`exists_mulEquiv_mrange_eq_mgraph` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike`	`mrange` `instMonoidHomClass` `mgraph` `MulEquiv.toMonoidHom`	—	`instMonoidHomClass` `exists_mrange_eq_mgraph` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `SetLike.ext_iff` `map_mul'`
`exists_mulEquiv_range_eq_graph` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Prod.instMulOneClass` `instFunLike`	`range` `Prod.instGroup` `graph` `MulEquiv.toMonoidHom`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `instMonoidHomClass` `exists_mulEquiv_mrange_eq_mgraph`
`exists_range_eq_graph` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Prod.instMulOneClass` `instFunLike`	`range` `Prod.instGroup` `graph`	—	`instMonoidHomClass` `exists_mrange_eq_mgraph`
`graph_eq_range_prod` 📖	mathematical	—	`graph` `range` `Prod.instGroup` `prod` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `id` `MulOneClass.toMulOne`	—	`Subgroup.ext`
`graph_toSubmonoid` 📖	mathematical	—	`Subgroup.toSubmonoid` `Prod.instGroup` `graph` `mgraph` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mem_graph` 📖	mathematical	—	`Subgroup` `Prod.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `graph` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike`	—	—
`mem_mgraph` 📖	mathematical	—	`Submonoid` `Prod.instMulOneClass` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `mgraph` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instFunLike`	—	—
`mgraph_eq_mrange_prod` 📖	mathematical	—	`mgraph` `mrange` `Monoid.toMulOneClass` `Prod.instMulOneClass` `MonoidHom` `MulOneClass.toMulOne` `instFunLike` `instMonoidHomClass` `prod` `id`	—	`Submonoid.ext` `instMonoidHomClass`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_graph` 📖	mathematical	`Function.Bijective` `Subgroup` `Prod.instGroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MonoidHom.instFunLike` `subtype`	`MonoidHom.graph`	—	`Submonoid.exists_eq_mgraph`
`exists_mulEquiv_eq_graph` 📖	mathematical	`Function.Bijective` `Subgroup` `Prod.instGroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `MonoidHom.instFunLike` `subtype`	`MonoidHom.graph` `MulEquiv.toMonoidHom`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Submonoid.exists_mulEquiv_eq_mgraph`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_mgraph` 📖	mathematical	`Function.Bijective` `Submonoid` `Prod.instMulOneClass` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `toMulOneClass` `MonoidHom.instFunLike` `subtype`	`MonoidHom.mgraph`	—	`MonoidHom.instMonoidHomClass` `mrange_subtype` `MonoidHom.exists_mrange_eq_mgraph` `Function.Bijective.surjective` `Function.Bijective.injective`
`exists_mulEquiv_eq_mgraph` 📖	mathematical	`Function.Bijective` `Submonoid` `Prod.instMulOneClass` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `toMulOneClass` `MonoidHom.instFunLike` `subtype`	`MonoidHom.mgraph` `MulEquiv.toMonoidHom`	—	`MonoidHom.instMonoidHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `mrange_subtype` `MonoidHom.exists_mulEquiv_mrange_eq_mgraph` `Function.Bijective.surjective` `Function.Bijective.injective`

---

← Back to Index