Documentation Verification Report

Duality

📁 Source: Mathlib/GroupTheory/FiniteAbelian/Duality.lean

Statistics

Metric	Count
Definitions `monoidHomMonoidHomEquiv`, `subgroupOrderIsoSubgroupMonoidHom`	2
Theorems `apply_monoidHomMonoidHomEquiv`, `card_monoidHom_of_hasEnoughRootsOfUnity`, `exists_apply_ne_one_of_hasEnoughRootsOfUnity`, `forall_apply_eq_apply_iff`, `forall_monoidHom_apply_eq_one_iff`, `mem_subgroupOrderIsoSubgroupMonoidHom_iff`, `mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff`, `monoidHomMonoidHomEquiv_symm_apply_apply`, `monoidHom_mulEquiv_of_hasEnoughRootsOfUnity`, `restrict_surjective`	10
Total	12

CommGroup

Definitions

Name	Category	Theorems
`monoidHomMonoidHomEquiv` 📖	CompOp	2 math math: `apply_monoidHomMonoidHomEquiv`, `monoidHomMonoidHomEquiv_symm_apply_apply`
`subgroupOrderIsoSubgroupMonoidHom` 📖	CompOp	2 math math: `mem_subgroupOrderIsoSubgroupMonoidHom_iff`, `mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_monoidHomMonoidHomEquiv` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `MulEquiv` `MonoidHom.instCommGroup` `Units.instCommGroupUnits` `MonoidHom.mul` `toCommMonoid` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `monoidHomMonoidHomEquiv`	—	`monoidHomMonoidHomEquiv_symm_apply_apply` `MulEquiv.symm_apply_apply`
`card_monoidHom_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`Nat.card` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass`	—	`Nat.card_congr` `monoidHom_mulEquiv_of_hasEnoughRootsOfUnity`
`exists_apply_ne_one_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass`	—	`Monoid.neZero_exponent_of_finite` `HasEnoughRootsOfUnity.of_dvd` `ZMod.exists_monoidHom_apply_ne_one` `HasEnoughRootsOfUnity.exists_primitiveRoot`
`forall_apply_eq_apply_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `MonoidHom.instFunLike`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `map_inv` `mul_inv_cancel` `exists_apply_ne_one_of_hasEnoughRootsOfUnity`
`forall_monoidHom_apply_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `Units.instOne` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	—	`Subgroup.normal_of_comm` `HasEnoughRootsOfUnity.of_dvd` `Monoid.neZero_exponent_of_finite` `Group.exponent_quotient_dvd` `forall_apply_eq_apply_iff` `Subgroup.finite_quotient_of_finiteIndex` `Subgroup.finiteIndex_of_finite` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass`
`mem_subgroupOrderIsoSubgroupMonoidHom_iff` 📖	mathematical	—	`MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `Subgroup` `MonoidHom.instCommGroup` `Units.instCommGroupUnits` `SetLike.instMembership` `Subgroup.instSetLike` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `OrderDual.instLE` `instFunLikeOrderIso` `subgroupOrderIsoSubgroupMonoidHom` `MonoidHom.instFunLike` `Units.instOne`	—	—
`mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff` 📖	mathematical	—	`Subgroup` `toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `DFunLike.coe` `OrderIso` `OrderDual` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMulOneClass` `MonoidHom.instCommGroup` `Units.instCommGroupUnits` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `instFunLikeOrderIso` `OrderIso.symm` `subgroupOrderIsoSubgroupMonoidHom` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `MonoidHom.instFunLike` `Units.instOne`	—	—
`monoidHomMonoidHomEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `MonoidHom.instCommGroup` `Units.instCommGroupUnits` `MonoidHom.instFunLike` `MulEquiv` `MulOne.toMul` `MonoidHom.mul` `toCommMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `monoidHomMonoidHomEquiv`	—	—
`monoidHom_mulEquiv_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`MulEquiv` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Units.instMulOneClass` `MonoidHom.mul` `toCommMonoid` `Units.instCommGroupUnits` `MulOne.toMul`	—	`equiv_prod_multiplicative_zmod_of_finite` `NeZero.of_gt` `Nat.instCanonicallyOrderedAdd` `Nat.card_eq_fintype_card` `Fintype.card_multiplicative` `ZMod.card` `Finite.of_fintype` `HasEnoughRootsOfUnity.of_dvd` `Monoid.neZero_exponent_of_finite` `IsCyclic.monoidHom_equiv_self` `instFiniteMultiplicative` `isCyclic_multiplicative` `ZMod.instIsAddCyclic`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrict_surjective` 📖	mathematical	—	`MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SubmonoidClass.toMulOneClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `DFunLike.coe` `instCommMonoid` `instFunLike` `restrictHom`	—	`Subgroup.instFiniteSubtypeMem` `HasEnoughRootsOfUnity.of_dvd` `Monoid.neZero_exponent_of_finite` `Monoid.exponent_submonoid_dvd` `Subgroup.normal_of_comm` `Group.exponent_quotient_dvd` `surjective_of_card_ker_le_div` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `instFiniteMonoidHomUnitsOfHasEnoughRootsOfUnityExponent` `le_of_eq` `CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity` `Subgroup.card_eq_card_quotient_mul_card_subgroup` `mul_div_cancel_right₀` `Nat.instMulDivCancelClass` `Fintype.card_ne_zero` `One.instNonempty` `Fintype.card_eq_nat_card` `Subgroup.finite_quotient_of_finiteIndex` `Subgroup.finiteIndex_of_finite` `Nat.card_congr`

---

← Back to Index