Documentation Verification Report

Duality

📁 Source: Mathlib/NumberTheory/MulChar/Duality.lean

Statistics

Metric	Count
Definitions `mulCharEquiv`, `subgroupOrderIsoSubgroupMulChar`	2
Theorems `apply_mulCharEquiv`, `card_eq_card_units_of_hasEnoughRootsOfUnity`, `exists_apply_ne_one_iff_exists_monoidHom`, `exists_apply_ne_one_of_hasEnoughRootsOfUnity`, `finite`, `mem_subgroupOrderIsoSubgroupMulChar_iff`, `mem_subgroupOrderIsoSubgroupMulChar_symm_iff`, `mulCharEquiv_symm_apply_apply`, `mulEquiv_units`, `restrictHom_surjective`	10
Total	12

MulChar

Definitions

Name	Category	Theorems
`mulCharEquiv` 📖	CompOp	2 math math: `mulCharEquiv_symm_apply_apply`, `apply_mulCharEquiv`
`subgroupOrderIsoSubgroupMulChar` 📖	CompOp	2 math math: `mem_subgroupOrderIsoSubgroupMulChar_symm_iff`, `mem_subgroupOrderIsoSubgroupMulChar_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mulCharEquiv` 📖	mathematical	—	`DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `instFunLike` `Units.val` `CommMonoid.toMonoid` `MulEquiv` `CommGroup.toCommMonoid` `commGroup` `Units` `hasMul` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulCharEquiv`	—	`mulCharEquiv_symm_apply_apply` `MulEquiv.symm_apply_apply`
`card_eq_card_units_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`Nat.card` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Units` `CommMonoid.toMonoid`	—	`Nat.card_congr` `mulEquiv_units`
`exists_apply_ne_one_iff_exists_monoidHom` 📖	mathematical	—	`MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MonoidHom` `Units` `CommMonoid.toMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `coe_toUnitHom` `Units.ext_iff` `equivToUnitHom_symm_coe`
`exists_apply_ne_one_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	—	`exists_apply_ne_one_iff_exists_monoidHom` `CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity` `instFiniteUnits` `Mathlib.Tactic.Contrapose.contrapose₄` `IsUnit.unit_spec` `Units.val_eq_one` `map_nonunit` `zero_ne_one` `NeZero.one`
`finite` 📖	mathematical	—	`Finite` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	—	`Finite.of_equiv` `instFiniteMonoidHomUnits`
`mem_subgroupOrderIsoSubgroupMulChar_iff` 📖	mathematical	—	`MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Subgroup` `CommGroup.toGroup` `commGroup` `SetLike.instMembership` `Subgroup.instSetLike` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderIso` `Units` `CommMonoid.toMonoid` `Units.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `OrderDual.instLE` `instFunLikeOrderIso` `subgroupOrderIsoSubgroupMulChar` `instFunLike` `Units.val` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`subgroupOrderIsoSubgroupMulChar.eq_1` `OrderIso.trans_apply` `OrderIso.dual_apply` `MulEquiv.coe_mapSubgroup` `OrderDual.ofDual_toDual` `Subgroup.mem_map_equiv` `coe_equivToUnitHom`
`mem_subgroupOrderIsoSubgroupMulChar_symm_iff` 📖	mathematical	—	`Units` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `DFunLike.coe` `OrderIso` `OrderDual` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `CommGroup.toGroup` `commGroup` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `instFunLikeOrderIso` `OrderIso.symm` `subgroupOrderIsoSubgroupMulChar` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `instFunLike` `Units.val` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`coe_equivToUnitHom`
`mulCharEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `commGroup` `instFunLike` `MulEquiv` `Units` `CommMonoid.toMonoid` `Units.instMul` `hasMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulCharEquiv` `Units.val`	—	`Group.isUnit` `mulEquivToUnitHom_apply` `coe_equivToUnitHom`
`mulEquiv_units` 📖	mathematical	—	`MulEquiv` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Units` `CommMonoid.toMonoid` `hasMul` `Units.instMul`	—	`CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity` `instFiniteUnits`
`restrictHom_surjective` 📖	mathematical	—	`MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `SubmonoidClass.toCommMonoid` `Submonoid.instSubmonoidClass` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `restrictHom`	—	`Submonoid.instSubmonoidClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidHom.restrict_surjective` `instFiniteUnits` `ext` `restrictHom_apply` `restrict_ofUnitHom` `MonoidHom.restrictHom_apply` `equivToUnitHom_symm_coe` `MulEquiv.apply_symm_apply` `coe_equivToUnitHom`

---

← Back to Index