Documentation Verification Report

NoncommCoprod

📁 Source: Mathlib/GroupTheory/NoncommCoprod.lean

Statistics

Metric	Count
Definitions `noncommCoprod`, `noncommCoprod`, `noncommCoprod`, `noncommCoprod`	4
Theorems `comp_noncommCoprod`, `noncommCoprod_apply`, `noncommCoprod_apply'`, `comp_noncommCoprod`, `noncommCoprod_apply`, `noncommCoprod_apply'`, `noncommCoprod_comp_inl`, `noncommCoprod_comp_inr`, `noncommCoprod_inl_inr`, `noncommCoprod_unique`, `comp_noncommCoprod`, `noncommCoprod_apply`, `noncommCoprod_apply'`, `noncommCoprod_comp_inl`, `noncommCoprod_comp_inr`, `noncommCoprod_injective`, `noncommCoprod_inl_inr`, `noncommCoprod_range`, `noncommCoprod_unique`, `comp_noncommCoprod`, `noncommCoprod_apply`, `noncommCoprod_apply'`	22
Total	26

AddHom

Definitions

Name	Category	Theorems
`noncommCoprod` 📖	CompOp	3 math math: `comp_noncommCoprod`, `noncommCoprod_apply'`, `noncommCoprod_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_noncommCoprod` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd` `DFunLike.coe` `AddHom` `funLike`	`comp` `Prod.instAdd` `noncommCoprod` `AddCommute.map` `addHomClass`	—	`ext` `AddCommute.map` `addHomClass` `map_add`
`noncommCoprod_apply` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd` `DFunLike.coe` `AddHom` `funLike`	`Prod.instAdd` `noncommCoprod`	—	—
`noncommCoprod_apply'` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd` `DFunLike.coe` `AddHom` `funLike`	`Prod.instAdd` `noncommCoprod`	—	`noncommCoprod_apply`

AddMonoidHom

Definitions

Name	Category	Theorems
`noncommCoprod` 📖	CompOp	7 math math: `comp_noncommCoprod`, `noncommCoprod_inl_inr`, `noncommCoprod_comp_inl`, `noncommCoprod_unique`, `noncommCoprod_apply'`, `noncommCoprod_comp_inr`, `noncommCoprod_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_noncommCoprod` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`comp` `Prod.instAddZeroClass` `noncommCoprod` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass`	—	`ext` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `map_add`
`noncommCoprod_apply` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`Prod.instAddZeroClass` `noncommCoprod`	—	—
`noncommCoprod_apply'` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`Prod.instAddZeroClass` `noncommCoprod`	—	`noncommCoprod_apply`
`noncommCoprod_comp_inl` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`comp` `Prod.instAddZeroClass` `noncommCoprod` `inl`	—	`ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass` `add_zero`
`noncommCoprod_comp_inr` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `instFunLike`	`comp` `Prod.instAddZeroClass` `noncommCoprod` `inr`	—	`ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass` `zero_add`
`noncommCoprod_inl_inr` 📖	mathematical	—	`noncommCoprod` `AddMonoid.toAddZeroClass` `Prod.instAddMonoid` `inl` `inr` `addCommute_inl_inr` `id` `AddZeroClass.toAddZero` `Prod.instAddZeroClass`	—	`noncommCoprod_unique`
`noncommCoprod_unique` 📖	mathematical	—	`noncommCoprod` `comp` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `inl` `inr` `AddCommute.map` `AddMonoidHom` `Prod.instAdd` `AddZero.toAdd` `DFunLike.coe` `instFunLike` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `addCommute_inl_inr`	—	`ext` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `addCommute_inl_inr` `map_add` `add_zero` `zero_add`

MonoidHom

Definitions

Name	Category	Theorems
`noncommCoprod` 📖	CompOp	9 math math: `noncommCoprod_comp_inr`, `noncommCoprod_apply`, `noncommCoprod_range`, `noncommCoprod_unique`, `noncommCoprod_inl_inr`, `noncommCoprod_comp_inl`, `noncommCoprod_injective`, `noncommCoprod_apply'`, `comp_noncommCoprod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_noncommCoprod` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`comp` `Prod.instMulOneClass` `noncommCoprod` `Commute.map` `MonoidHomClass.toMulHomClass` `instMonoidHomClass`	—	`ext` `Commute.map` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `map_mul`
`noncommCoprod_apply` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`Prod.instMulOneClass` `noncommCoprod`	—	—
`noncommCoprod_apply'` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`Prod.instMulOneClass` `noncommCoprod`	—	`noncommCoprod_apply`
`noncommCoprod_comp_inl` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`comp` `Prod.instMulOneClass` `noncommCoprod` `inl`	—	`ext` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `mul_one`
`noncommCoprod_comp_inr` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `instFunLike`	`comp` `Prod.instMulOneClass` `noncommCoprod` `inr`	—	`ext` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `one_mul`
`noncommCoprod_injective` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `instFunLike`	`Prod.instMulOneClass` `noncommCoprod` `Disjoint` `Subgroup` `Subgroup.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `range`	—	`instMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `mul_one` `one_mul` `map_inv` `mul_inv_cancel` `inv_eq_iff_mul_eq_one`
`noncommCoprod_inl_inr` 📖	mathematical	—	`noncommCoprod` `Monoid.toMulOneClass` `Prod.instMonoid` `inl` `inr` `commute_inl_inr` `id` `MulOneClass.toMulOne` `Prod.instMulOneClass`	—	`noncommCoprod_unique`
`noncommCoprod_range` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MonoidHom` `instFunLike`	`range` `Prod.instGroup` `noncommCoprod` `Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Subgroup.instCompleteLattice`	—	`le_antisymm` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Subgroup.mem_sup_left` `Subgroup.mem_sup_right` `sup_le_iff` `noncommCoprod_apply` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `mul_one` `one_mul`
`noncommCoprod_unique` 📖	mathematical	—	`noncommCoprod` `comp` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `inl` `inr` `Commute.map` `MonoidHom` `Prod.instMul` `MulOne.toMul` `DFunLike.coe` `instFunLike` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `commute_inl_inr`	—	`ext` `Commute.map` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `commute_inl_inr` `mul_one` `one_mul`

MulHom

Definitions

Name	Category	Theorems
`noncommCoprod` 📖	CompOp	3 math math: `noncommCoprod_apply`, `noncommCoprod_apply'`, `comp_noncommCoprod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_noncommCoprod` 📖	mathematical	`Commute` `Semigroup.toMul` `DFunLike.coe` `MulHom` `funLike`	`comp` `Prod.instMul` `noncommCoprod` `Commute.map` `mulHomClass`	—	`ext` `Commute.map` `mulHomClass` `map_mul`
`noncommCoprod_apply` 📖	mathematical	`Commute` `Semigroup.toMul` `DFunLike.coe` `MulHom` `funLike`	`Prod.instMul` `noncommCoprod`	—	—
`noncommCoprod_apply'` 📖	mathematical	`Commute` `Semigroup.toMul` `DFunLike.coe` `MulHom` `funLike`	`Prod.instMul` `noncommCoprod`	—	`noncommCoprod_apply`

---

← Back to Index