Documentation Verification Report

CircleAddChar

📁 Source: Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

Statistics

Metric	Count
Definitions `toCircle_addChar`, `rootsOfUnityAddChar`, `stdAddChar`, `toCircle`, `rootsOfUnityCircleEquiv`, `rootsOfUnitytoCircle`	6
Theorems `injective_stdAddChar`, `injective_toCircle`, `isPrimitive_stdAddChar`, `rootsOfUnityAddChar_val`, `stdAddChar_apply`, `stdAddChar_coe`, `toCircle_apply`, `toCircle_eq_circleExp`, `toCircle_intCast`, `toCircle_natCast`, `bijective_rootsOfUnityAddChar`, `instHasEnoughRootsOfUnityCircle`, `rootsOfUnityCircleEquiv_apply`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar`	15
Total	21

AddCircle

Definitions

Name	Category	Theorems
`toCircle_addChar` 📖	CompOp	—

ZMod

Definitions

Name	Category	Theorems
`rootsOfUnityAddChar` 📖	CompOp	4 math math: `bijective_rootsOfUnityAddChar`, `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `rootsOfUnityAddChar_val`
`stdAddChar` 📖	CompOp	11 math math: `LFunction_stdAddChar_eq_expZeta`, `invDFT_apply`, `stdAddChar_coe`, `isPrimitive_stdAddChar`, `dft_apply`, `DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum`, `invDFT_def`, `DirichletCharacter.fourierTransform_eq_gaussSum_mulShift`, `injective_stdAddChar`, `dft_def`, `stdAddChar_apply`
`toCircle` 📖	CompOp	8 math math: `toCircle_intCast`, `toCircle_natCast`, `injective_toCircle`, `toCircle_apply`, `dft_eq_fourier`, `rootsOfUnityAddChar_val`, `toCircle_eq_circleExp`, `stdAddChar_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_stdAddChar` 📖	mathematical	—	`ZMod` `Complex` `DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `AddChar.instFunLike` `stdAddChar`	—	`Subtype.coe_injective` `injective_toCircle`
`injective_toCircle` 📖	mathematical	—	`ZMod` `Circle` `DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `toCircle`	—	`AddSubgroup.normal_of_comm` `AddCircle.injective_toCircle` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `toAddCircle_injective`
`isPrimitive_stdAddChar` 📖	mathematical	—	`AddChar.IsPrimitive` `ZMod` `commRing` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `stdAddChar`	—	`AddChar.zmod_char_primitive_of_eq_one_only_at_zero` `injective_stdAddChar` `AddChar.map_zero_eq_one`
`rootsOfUnityAddChar_val` 📖	mathematical	—	`Units.val` `Circle` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `Circle.instCommGroup` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `AddChar.instFunLike` `rootsOfUnityAddChar` `CommGroup.toGroup` `toCircle`	—	—
`stdAddChar_apply` 📖	mathematical	—	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `AddChar.instFunLike` `stdAddChar` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `toCircle`	—	—
`stdAddChar_coe` 📖	mathematical	—	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `AddChar.instFunLike` `stdAddChar` `AddGroupWithOne.toIntCast` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Complex.instIntCast`	—	`Nat.instAtLeastTwoHAddOfNat` `toCircle_intCast`
`toCircle_apply` 📖	mathematical	—	`Complex` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `toCircle` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `val`	—	`Nat.instAtLeastTwoHAddOfNat` `toCircle_natCast` `natCast_zmod_val`
`toCircle_eq_circleExp` 📖	mathematical	—	`DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `toCircle` `ContinuousMap` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `Circle.exp` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `val`	—	`Circle.ext` `Nat.instAtLeastTwoHAddOfNat` `toCircle_apply` `Circle.coe_exp` `Complex.ofReal_mul` `Complex.ofReal_div` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul`
`toCircle_intCast` 📖	mathematical	—	`Complex` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `toCircle` `AddGroupWithOne.toIntCast` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Complex.instIntCast`	—	`Nat.instAtLeastTwoHAddOfNat` `toCircle.eq_1` `AddChar.compAddMonoidHom_apply` `AddCircle.toCircle_zero` `AddCircle.toCircle_add` `AddCircle.toCircle_addChar.eq_1` `AddCircle.scaled_exp_map_periodic` `AddCircle.toCircle.eq_1` `AddSubgroup.normal_of_comm` `toAddCircle_intCast` `Function.Periodic.lift_coe` `Circle.coe_exp` `Complex.ofReal_mul` `Complex.ofReal_div` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero`
`toCircle_natCast` 📖	mathematical	—	`Complex` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `toCircle` `AddMonoidWithOne.toNatCast` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Nat.instAtLeastTwoHAddOfNat` `Int.cast_natCast` `toCircle_intCast`

(root)

Definitions

Name	Category	Theorems
`rootsOfUnityCircleEquiv` 📖	CompOp	3 math math: `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `rootsOfUnityCircleEquiv_apply`
`rootsOfUnitytoCircle` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_rootsOfUnityAddChar` 📖	mathematical	—	`Function.Bijective` `ZMod` `Units` `Circle` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `Circle.instCommGroup` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `DFunLike.coe` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `AddChar.instFunLike` `ZMod.rootsOfUnityAddChar`	—	`EquivLike.toEmbeddingLike` `ZMod.injective_toCircle` `Function.Surjective.of_comp_left` `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar` `MulEquiv.injective`
`instHasEnoughRootsOfUnityCircle` 📖	mathematical	—	`HasEnoughRootsOfUnity` `Circle` `CommGroup.toCommMonoid` `Circle.instCommGroup`	—	`MulEquiv.hasEnoughRootsOfUnity` `IsSepClosed.hasEnoughRootsOfUnity` `NeZero.charZero` `Complex.instCharZero` `IsSepClosed.of_isAlgClosed` `Complex.isAlgClosed`
`rootsOfUnityCircleEquiv_apply` 📖	mathematical	—	`Units.val` `Complex` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Complex.commRing` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `DFunLike.coe` `MulEquiv` `Circle` `CommGroup.toCommMonoid` `Circle.instCommGroup` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `rootsOfUnityCircleEquiv` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	—
`rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val` 📖	mathematical	—	`Units.val` `Complex` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Complex.commRing` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `DFunLike.coe` `MulEquiv` `Circle` `CommGroup.toCommMonoid` `Circle.instCommGroup` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `rootsOfUnityCircleEquiv` `AddChar` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `AddChar.instFunLike` `ZMod.rootsOfUnityAddChar` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `ZMod.val`	—	`Nat.instAtLeastTwoHAddOfNat` `ZMod.rootsOfUnityAddChar_val` `ZMod.natCast_zmod_val`
`surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar` 📖	mathematical	—	`ZMod` `Units` `Complex` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Complex.commRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `Circle` `CommGroup.toCommMonoid` `Circle.instCommGroup` `DFunLike.coe` `MulEquiv` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `rootsOfUnityCircleEquiv` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `AddChar.instFunLike` `ZMod.rootsOfUnityAddChar`	—	`Nat.instAtLeastTwoHAddOfNat` `Complex.mem_rootsOfUnity` `ZMod.rootsOfUnityAddChar_val` `ZMod.toCircle_natCast` `mul_div_assoc`

---

← Back to Index