Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions `equiv_rootsOfUnity`, `instStarMul`, `ofRootOfUnity`, `restrictHom`, `starComp`	5
Theorems `apply_mem_algebraAdjoin`, `apply_mem_algebraAdjoin_of_pow_eq_one`, `apply_mem_rootsOfUnity`, `apply_mem_rootsOfUnity_of_pow_eq_one`, `apply_mem_rootsOfUnity_orderOf`, `eq_iff`, `exists_apply_eq_pow`, `exists_mulChar_orderOf`, `exists_mulChar_orderOf_eq_card_units`, `ofRootOfUnity_spec`, `orderOf_dvd_card_sub_one`, `restrictHom_apply`, `restrict_ofUnitHom`, `starComp_apply`, `star_apply`, `star_apply'`, `star_eq_inv`	17
Total	22

MulChar

Definitions

Name	Category	Theorems
`equiv_rootsOfUnity` 📖	CompOp	—
`instStarMul` 📖	CompOp	2 math math: `star_apply`, `star_eq_inv`
`ofRootOfUnity` 📖	CompOp	1 math math: `ofRootOfUnity_spec`
`restrictHom` 📖	CompOp	2 math math: `restrictHom_surjective`, `restrictHom_apply`
`starComp` 📖	CompOp	1 math math: `starComp_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_algebraAdjoin` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `orderOf` `MulChar` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup`	`Subalgebra` `Int.instCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toIntAlgebra` `CommRing.toRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `instFunLike`	—	`LT.lt.ne'` `orderOf_pos` `instFiniteUnits` `apply_mem_algebraAdjoin_of_pow_eq_one` `pow_orderOf_eq_one`
`apply_mem_algebraAdjoin_of_pow_eq_one` 📖	mathematical	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `hasOne` `IsPrimitiveRoot`	`Subalgebra` `Int.instCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toIntAlgebra` `CommRing.toRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `instFunLike`	—	`eq_or_ne` `Subalgebra.zero_mem` `map_zero` `EuclideanDomain.toNontrivial` `apply_mem_rootsOfUnity_of_pow_eq_one` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `Units.val_pow_eq_pow_val` `Units.ext_iff` `mem_rootsOfUnity` `Subalgebra.pow_mem` `Algebra.self_mem_adjoin_singleton`
`apply_mem_rootsOfUnity` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Subgroup` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `Fintype.card` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Equiv` `MulChar` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivToUnitHom`	—	`mem_rootsOfUnity` `map_pow` `MonoidHom.instMonoidHomClass` `MonoidHom.map_one` `pow_card_eq_one`
`apply_mem_rootsOfUnity_of_pow_eq_one` 📖	mathematical	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `hasOne`	`Units` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `Units.val` `DFunLike.coe` `MulChar` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `instFunLike`	—	`apply_mem_rootsOfUnity_orderOf` `rootsOfUnity_le_of_dvd` `orderOf_dvd_of_pow_eq_one`
`apply_mem_rootsOfUnity_orderOf` 📖	mathematical	—	`Units` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `orderOf` `MulChar` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `Units.val` `DFunLike.coe` `instFunLike`	—	`IsUnit.map` `MulCharClass.toMonoidHomClass` `instMulCharClass` `Ne.isUnit` `mem_rootsOfUnity` `Units.ext_iff` `Units.val_pow_eq_pow_val` `Units.val_one` `IsUnit.unit_spec` `pow_apply'` `LT.lt.ne'` `orderOf_pos` `instFiniteUnits` `pow_orderOf_eq_one` `isUnit_iff_ne_zero` `one_apply_coe`
`eq_iff` 📖	mathematical	`Units` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`DFunLike.coe` `MulChar` `instFunLike` `Units.val` `CommMonoid.toMonoid`	—	`Equiv.apply_eq_iff_eq` `MonoidHom.eq_iff_eq_on_generator` `coe_equivToUnitHom` `Units.ext_iff`
`exists_apply_eq_pow` 📖	mathematical	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `hasOne` `IsPrimitiveRoot`	`DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`apply_mem_rootsOfUnity_of_pow_eq_one` `mem_rootsOfUnity'` `IsPrimitiveRoot.eq_pow_of_pow_eq_one`
`exists_mulChar_orderOf` 📖	mathematical	`Fintype.card` `IsPrimitiveRoot` `CommRing.toCommMonoid`	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup`	—	`LT.lt.false` `LT.lt.trans_le` `Fintype.one_lt_card` `EuclideanDomain.toNontrivial` `instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteUnits` `Finite.of_fintype` `IsPrimitiveRoot.isUnit` `LT.lt.ne'` `Units.ext_iff` `IsPrimitiveRoot.pow_eq_one_iff_dvd` `Fintype.card_units` `mem_rootsOfUnity` `MulEquiv.orderOf_eq` `orderOf_eq_iff` `Units.ext` `IsPrimitiveRoot.pow_eq_one` `LE.le.trans_lt` `IsPrimitiveRoot.dvd_of_pow_eq_one`
`exists_mulChar_orderOf_eq_card_units` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Fintype.card` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFintypeUnitsOfDecidableEq`	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `Fintype.card` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFintypeUnitsOfDecidableEq`	—	`exists_mulChar_orderOf` `Fintype.card_units` `dvd_refl`
`ofRootOfUnity_spec` 📖	mathematical	`Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Subgroup` `CommMonoid.toMonoid` `CommMonoidWithZero.toCommMonoid` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `Fintype.card` `instFintypeUnitsOfDecidableEq` `Subgroup.zpowers`	`DFunLike.coe` `MulChar` `instFunLike` `ofRootOfUnity` `Units.val` `CommMonoid.toMonoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`equivToUnitHom_symm_coe` `monoidHomOfForallMemZpowers_apply_gen`
`orderOf_dvd_card_sub_one` 📖	mathematical	—	`orderOf` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `Fintype.card`	—	`Fintype.card_units` `orderOf_dvd_of_pow_eq_one` `pow_card_eq_one`
`restrictHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulChar` `SetLike.instMembership` `SubmonoidClass.toCommMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `commGroup` `MonoidHom.instFunLike` `restrictHom` `restrict`	—	—
`restrict_ofUnitHom` 📖	mathematical	—	`restrict` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid.instSetLike` `Submonoid.instSubmonoidClass` `ofUnitHom` `SetLike.instMembership` `SubmonoidClass.toCommMonoid` `MonoidHom.comp` `Units` `Subgroup` `Units.instGroup` `Subgroup.instSetLike` `Submonoid.units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulOneClass.toMulOne` `Units.instMulOneClass` `SubmonoidClass.toMulOneClass` `SubgroupClass.toSubmonoidClass` `Group.toDivInvMonoid` `Subgroup.instSubgroupClass` `MonoidHom.restrict` `MonoidHomClass.toMonoidHom` `MulEquiv` `Submonoid.toMonoid` `Units.instMul` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `DivInvMonoid.toMonoid` `Subgroup.toGroup` `MulEquiv.instMulEquivClass` `MulEquiv.symm` `Submonoid.unitsEquivUnitsType`	—	`ext` `Submonoid.instSubmonoidClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `restrict_apply` `equivToUnitHom_symm_coe` `Submonoid.val_unitsEquivUnitsType_symm_apply_coe`
`starComp_apply` 📖	mathematical	—	`DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `instFunLike` `starComp` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `starRingEnd`	—	—
`star_apply` 📖	mathematical	—	`DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `instFunLike` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `hasMul` `instStarMul` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	—	—
`star_apply'` 📖	mathematical	—	`Star.star` `Complex` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `StarRing.toStarAddMonoid` `Complex.instStarRing` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `instFunLike` `hasInv`	—	—
`star_eq_inv` 📖	mathematical	—	`Star.star` `MulChar` `CommRing.toCommMonoid` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `hasMul` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Complex.commRing` `instStarMul` `Complex.instStarRing` `hasInv`	—	`nonempty_fintype` `ext` `inv_apply_eq_inv'` `Complex.inv_eq_conj` `Complex.norm_eq_one_of_mem_rootsOfUnity` `Fintype.instNeZeroNatCardOfNonempty` `apply_mem_rootsOfUnity`

---

← Back to Index