Circle

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

Statistics

Metric	Count
Definitions `homeomorphCircle`, `homeomorphCircle'`, `toCircle`, `Circle`, `argEquiv`, `argPartialEquiv`, `toCircle`	7
Theorems `continuous_toCircle`, `homeomorphCircle'_apply`, `homeomorphCircle'_apply_mk`, `homeomorphCircle'_symm_apply`, `homeomorphCircle_apply`, `injective_toCircle`, `scaled_exp_map_periodic`, `toCircle_add`, `toCircle_apply_mk`, `toCircle_neg`, `toCircle_nsmul`, `toCircle_zero`, `toCircle_zsmul`, `argEquiv_apply_coe`, `argEquiv_symm_apply`, `argPartialEquiv_apply`, `argPartialEquiv_source`, `argPartialEquiv_symm_apply`, `argPartialEquiv_target`, `arg_eq_arg`, `arg_exp`, `exp_add_two_pi`, `exp_arg`, `exp_eq_exp`, `exp_eq_one`, `exp_inj`, `exp_int_mul_two_pi`, `exp_sub_two_pi`, `exp_two_pi`, `exp_two_pi_mul_int`, `injective_arg`, `invOn_arg_exp`, `isAddQuotientCoveringMap_exp`, `isCoveringMap_exp`, `isQuotientCoveringMap_npow`, `isQuotientCoveringMap_zpow`, `leftInverse_exp_arg`, `periodic_exp`, `surjOn_exp_neg_pi_pi`, `arg_toCircle`, `coe_toCircle`, `toCircle_add`, `toCircle_coe`, `toCircle_neg`, `toCircle_zero`, `isLocalHomeomorph_circleExp`	46
Total	53

AddCircle

Definitions

Name	Category	Theorems
`homeomorphCircle` 📖	CompOp	1 math math: `homeomorphCircle_apply`
`homeomorphCircle'` 📖	CompOp	3 math math: `homeomorphCircle'_apply_mk`, `homeomorphCircle'_symm_apply`, `homeomorphCircle'_apply`
`toCircle` 📖	CompOp	15 math math: `toCircle_add`, `fourier_one`, `fourier_neg'`, `injective_toCircle`, `toCircle_zero`, `continuous_toCircle`, `toCircle_zsmul`, `fourier_apply`, `toCircle_apply_mk`, `fourier_zero'`, `fourier_coe_apply'`, `fourier_add'`, `toCircle_nsmul`, `homeomorphCircle_apply`, `toCircle_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_toCircle` 📖	mathematical	—	`Continuous` `AddCircle` `Real` `Real.instAddCommGroup` `Circle` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `instTopologicalSpaceCircle` `toCircle`	—	`continuous_coinduced_dom` `Continuous.comp` `ContinuousMap.continuous` `Continuous.comp'` `Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.prodMk` `continuous_const`
`homeomorphCircle'_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Circle` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `instTopologicalSpaceCircle` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphCircle'` `Real.Angle.toCircle`	—	`Nat.instAtLeastTwoHAddOfNat`
`homeomorphCircle'_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Circle` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `instTopologicalSpaceCircle` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphCircle'` `ContinuousMap` `ContinuousMap.instFunLike` `Circle.exp`	—	`Nat.instAtLeastTwoHAddOfNat`
`homeomorphCircle'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Circle` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `instTopologicalSpaceCircle` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphCircle'` `Complex.arg` `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`	—	`Nat.instAtLeastTwoHAddOfNat`
`homeomorphCircle_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `AddCircle` `Real` `Real.instAddCommGroup` `Circle` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `instTopologicalSpaceCircle` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphCircle` `toCircle`	—	`QuotientAddGroup.induction_on` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `homeomorphCircle.eq_1` `Homeomorph.trans_apply` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_congr` `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` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf`
`injective_toCircle` 📖	mathematical	—	`AddCircle` `Real` `Real.instAddCommGroup` `Circle` `toCircle`	—	`QuotientAddGroup.induction_on` `Nat.instAtLeastTwoHAddOfNat` `Circle.exp_eq_exp` `QuotientAddGroup.eq` `zsmul_eq_mul` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Real.pi_pos` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `neg_eq_zero`
`scaled_exp_map_periodic` 📖	mathematical	—	`Function.Periodic` `Real` `Circle` `Real.instAdd` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `Circle.exp` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `div_zero` `add_zero` `MulZeroClass.zero_mul` `Circle.exp_zero` `mul_add` `Distrib.leftDistribClass` `div_mul_cancel₀` `Circle.periodic_exp`
`toCircle_add` 📖	mathematical	—	`toCircle` `AddCircle` `Real` `Real.instAddCommGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroupReal` `Circle` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup`	—	`QuotientAddGroup.induction_on` `Nat.instAtLeastTwoHAddOfNat` `mul_add` `Distrib.leftDistribClass` `Circle.exp_add`
`toCircle_apply_mk` 📖	mathematical	—	`toCircle` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `DFunLike.coe` `ContinuousMap` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `Circle.exp` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	—
`toCircle_neg` 📖	mathematical	—	`toCircle` `AddCircle` `Real` `Real.instAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `Circle` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Circle.instCommGroup`	—	`RightCancelSemigroup.toIsRightCancelMul` `AddSubgroup.normal_of_comm` `neg_add_cancel` `toCircle_zero` `inv_mul_cancel`
`toCircle_nsmul` 📖	mathematical	—	`toCircle` `AddCircle` `Real` `Real.instAddCommGroup` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupReal` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Circle` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup`	—	`zero_nsmul` `toCircle_zero` `pow_zero` `succ_nsmul` `toCircle_add` `pow_succ`
`toCircle_zero` 📖	mathematical	—	`toCircle` `AddCircle` `Real` `Real.instAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `Circle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Circle.instCommGroup`	—	`AddSubgroup.normal_of_comm` `QuotientAddGroup.mk_zero` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `Circle.exp_zero`
`toCircle_zsmul` 📖	mathematical	—	`toCircle` `AddCircle` `Real` `Real.instAddCommGroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `AddSubgroup.normal_of_comm` `Circle` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup`	—	`AddSubgroup.normal_of_comm` `natCast_zsmul` `toCircle_nsmul` `zpow_natCast` `negSucc_zsmul` `toCircle_neg` `zpow_negSucc`

Circle

Definitions

Name	Category	Theorems
`argEquiv` 📖	CompOp	2 math math: `argEquiv_symm_apply`, `argEquiv_apply_coe`
`argPartialEquiv` 📖	CompOp	4 math math: `argPartialEquiv_source`, `argPartialEquiv_target`, `argPartialEquiv_symm_apply`, `argPartialEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`argEquiv_apply_coe` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `DFunLike.coe` `Equiv` `Circle` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `argEquiv` `Complex.arg` `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`	—	—
`argEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `Real` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `Circle` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `argEquiv` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Set` `Set.instMembership`	—	—
`argPartialEquiv_apply` 📖	mathematical	—	`PartialEquiv.toFun` `Circle` `Real` `argPartialEquiv` `Complex` `Complex.arg` `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`	—	—
`argPartialEquiv_source` 📖	mathematical	—	`PartialEquiv.source` `Circle` `Real` `argPartialEquiv` `Set.univ`	—	—
`argPartialEquiv_symm_apply` 📖	mathematical	—	`PartialEquiv.toFun` `Real` `Circle` `PartialEquiv.symm` `argPartialEquiv` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp`	—	—
`argPartialEquiv_target` 📖	mathematical	—	`PartialEquiv.target` `Circle` `Real` `argPartialEquiv` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi`	—	—
`arg_eq_arg` 📖	mathematical	—	`Complex.arg` `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`	—	`injective_arg`
`arg_exp` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.pi` `Real.instLE`	`Complex.arg` `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` `ContinuousMap` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp`	—	`coe_exp` `Complex.exp_mul_I` `Complex.arg_cos_add_sin_mul_I`
`exp_add_two_pi` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`periodic_exp`
`exp_arg` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Complex.arg` `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`	—	`injective_arg` `arg_exp` `Complex.neg_pi_lt_arg` `Complex.arg_le_pi`
`exp_eq_exp` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instAdd` `Real.instMul` `Real.instIntCast` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `coe_exp` `Complex.exp_eq_exp_iff_exists_int` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Complex.I_ne_zero`
`exp_eq_one` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup` `Real.instMul` `Real.instIntCast` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Complex.ofReal_mul`
`exp_inj` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `AddCommGroup.ModEq` `Real.instAddCommMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `zsmul_eq_mul` `exp_sub`
`exp_int_mul_two_pi` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instMul` `Real.instIntCast` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup`	—	`ext` `Nat.instAtLeastTwoHAddOfNat` `exp_intCast_mul` `exp_two_pi` `one_zpow`
`exp_sub_two_pi` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instSub` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Function.Periodic.sub_eq` `Nat.instAtLeastTwoHAddOfNat` `periodic_exp`
`exp_two_pi` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `Function.Periodic.eq` `periodic_exp` `exp_zero`
`exp_two_pi_mul_int` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.instIntCast` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_comm` `exp_int_mul_two_pi`
`injective_arg` 📖	mathematical	—	`Circle` `Real` `Complex.arg` `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`	—	`Complex.ext_norm_arg` `norm_coe`
`invOn_arg_exp` 📖	mathematical	—	`Set.InvOn` `Real` `Circle` `Complex` `Complex.arg` `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` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `Set.univ`	—	`PartialEquiv.invOn`
`isAddQuotientCoveringMap_exp` 📖	mathematical	—	`IsAddQuotientCoveringMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `exp` `AddSubgroup` `Real.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `AddSubgroup.toAddGroup` `AddAction.instAddAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor`	—	`Nat.instAtLeastTwoHAddOfNat` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `ext` `AddCircle.scaled_exp_map_periodic` `div_self` `one_mul` `AddCircle.homeomorphCircle_apply` `Function.Periodic.lift.congr_simp` `IsAddQuotientCoveringMap.homeomorph_comp` `AddCircle.isAddQuotientCoveringMap_coe` `instIsTopologicalAddGroupReal` `Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples`
`isCoveringMap_exp` 📖	mathematical	—	`IsCoveringMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `exp`	—	`IsAddQuotientCoveringMap.isCoveringMap` `Nat.instAtLeastTwoHAddOfNat` `isAddQuotientCoveringMap_exp`
`isQuotientCoveringMap_npow` 📖	mathematical	—	`IsQuotientCoveringMap` `Circle` `instTopologicalSpaceCircle` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Monoid.toMulOneClass` `powMonoidHom` `CommGroup.toCommMonoid` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toMulAction`	—	`isQuotientCoveringMap_zpow`
`isQuotientCoveringMap_zpow` 📖	mathematical	—	`IsQuotientCoveringMap` `Circle` `instTopologicalSpaceCircle` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `zpowGroupHom` `CommGroup.toDivisionCommMonoid` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toMulAction`	—	`RCLike.charZero_rclike` `one_ne_zero` `NeZero.charZero_one` `Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom` `instIsTopologicalGroup` `Topology.IsQuotientMap.of_comp` `Homeomorph.continuous` `continuous_zpow` `AddSubgroup.normal_of_comm` `ext` `AddCircle.homeomorphCircle_apply` `AddCircle.toCircle_zsmul` `Topology.IsQuotientMap.comp` `Homeomorph.isQuotientMap` `IsUnit.isQuotientMap_zsmul` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `isQuotientMap_quotient_mk'` `Set.Finite.isDiscrete` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.Finite.of_preimage` `Set.ext` `AddCircle.injective_toCircle` `AddCircle.toCircle_zero` `AddCircle.finite_torsion_of_isSMulRegular_int` `zsmul_eq_mul` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `Homeomorph.surjective`
`leftInverse_exp_arg` 📖	mathematical	—	`Circle` `Real` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Complex` `Complex.arg` `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`	—	`exp_arg`
`periodic_exp` 📖	mathematical	—	`Function.Periodic` `Real` `Circle` `Real.instAdd` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `exp_eq_exp` `Int.cast_one` `one_mul`
`surjOn_exp_neg_pi_pi` 📖	mathematical	—	`Set.SurjOn` `Real` `Circle` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `exp` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `Set.univ`	—	`PartialEquiv.surjOn`

Real.Angle

Definitions

Name	Category	Theorems
`toCircle` 📖	CompOp	12 math math: `toCircle_add`, `Orientation.rotation_map_complex`, `coe_toCircle`, `toCircle_zero`, `arg_toCircle`, `toCircle_coe`, `Orientation.kahler_rotation_left'`, `Orientation.kahler_rotation_left`, `toCircle_neg`, `Orientation.kahler_rotation_right`, `AddCircle.homeomorphCircle'_apply`, `Complex.rotation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arg_toCircle` 📖	mathematical	—	`coe` `Complex.arg` `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` `toCircle`	—	`induction_on` `toCircle_coe` `Circle.coe_exp` `Complex.exp_mul_I` `Complex.ofReal_cos` `Complex.ofReal_sin` `cos_coe` `sin_coe` `Complex.arg_cos_add_sin_mul_I_coe_angle`
`coe_toCircle` 📖	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` `toCircle` `Complex.instAdd` `Complex.ofReal` `cos` `Complex.instMul` `sin` `Complex.I`	—	`induction_on` `Complex.exp_mul_I` `Complex.ofReal_cos` `Complex.ofReal_sin`
`toCircle_add` 📖	mathematical	—	`toCircle` `Real.Angle` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instNormedAddCommGroupAngle` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Circle` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup`	—	`induction_on` `Circle.exp_add`
`toCircle_coe` 📖	mathematical	—	`toCircle` `coe` `DFunLike.coe` `ContinuousMap` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `ContinuousMap.instFunLike` `Circle.exp`	—	—
`toCircle_neg` 📖	mathematical	—	`toCircle` `Real.Angle` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instNormedAddCommGroupAngle` `Circle` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Circle.instCommGroup`	—	`induction_on` `Circle.exp_neg`
`toCircle_zero` 📖	mathematical	—	`toCircle` `Real.Angle` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instNormedAddCommGroupAngle` `Circle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Circle.instCommGroup`	—	`coe_zero` `toCircle_coe` `Circle.exp_zero`

(root)

Definitions

Name	Category	Theorems
`Circle` 📖	CompOp	148 math math: `Circle.periodic_exp`, `Real.hasFDerivAt_fourierChar_neg_bilinear_left`, `Complex.UnitDisc.instIsScalarTower_circle`, `Circle.exp_arg`, `Circle.injective_arg`, `AddCircle.homeomorphCircle'_apply_mk`, `Real.fourierIntegral_eq`, `Real.Angle.toCircle_add`, `Real.fderiv_fourierChar_neg_bilinear_right_apply`, `Circle.exp_natCast_mul`, `AddCircle.toCircle_add`, `Complex.UnitDisc.instSMulCommClass_closedBall_circle`, `rotation_injective`, `Circle.starRingEnd_addChar`, `AddCircle.homeomorphCircle'_symm_apply`, `Circle.isAddQuotientCoveringMap_exp`, `tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support`, `rotation_apply`, `toMatrix_rotation`, `Circle.exp_eq_exp`, `Circle.exp_two_pi_mul_int`, `AddCircle.scaled_exp_map_periodic`, `Circle.argPartialEquiv_source`, `Circle.instIsScalarTower`, `Complex.UnitDisc.coe_smul_circle`, `Complex.UnitDisc.instIsScalarTower_circle_circle`, `Complex.UnitDisc.instSMulCommClass_circle_left`, `AddChar.zmod_add`, `instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle`, `tendsto_integral_exp_smul_cocompact`, `instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle`, `Real.fourier_real_eq`, `Circle.smul_def`, `Circle.exp_two_pi`, `Real.fourierIntegral_convergent_iff'`, `Real.Angle.toCircle_zero`, `Circle.exp_sub`, `Circle.isQuotientCoveringMap_zpow`, `Real.continuous_probChar`, `Circle.instSMulCommClass_left`, `Circle.exp_neg`, `Circle.instIsTopologicalGroup`, `Circle.coe_inv_eq_conj`, `Circle.coe_mul`, `Circle.coe_pow`, `Circle.exp_inj`, `fourierIntegral_eq_half_sub_half_period_translate`, `Circle.exp_add_two_pi`, `Circle.invOn_arg_exp`, `Circle.instSMulCommClass_right`, `Circle.instContinuousSMul`, `linear_isometry_complex`, `Real.Angle.toCircle_coe`, `Circle.star_addChar`, `rotationOf_rotation`, `bijective_rootsOfUnityAddChar`, `AddCircle.injective_toCircle`, `Real.fourier_eq`, `AddCircle.toCircle_zero`, `AddCircle.continuous_toCircle`, `Circle.exp_add`, `tendsto_integral_exp_smul_cocompact_of_inner_product`, `AddCircle.toCircle_zsmul`, `surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar`, `Circle.leftInverse_exp_arg`, `Circle.instIsUniformGroup`, `Circle.argEquiv_symm_apply`, `AddCircle.toCircle_apply_mk`, `Circle.isQuotientCoveringMap_npow`, `rotation_trans`, `instHasEnoughRootsOfUnityCircle`, `Real.probChar_apply'`, `Circle.instCompactSpace`, `Circle.exp_zero`, `Complex.UnitDisc.instSMulCommClass_circle_right`, `Real.fourierIntegral_convergent_iff`, `Real.hasDerivAt_fourierChar`, `linearEquiv_det_rotation`, `Circle.coe_eq_one`, `Real.fourierChar_apply`, `Real.fourier_bilin_convolution_eq_integral`, `Circle.exp_int_mul_two_pi`, `Real.tendsto_integral_exp_smul_cocompact`, `fourierIntegral_half_period_translate`, `Circle.surjOn_exp_neg_pi_pi`, `Circle.coe_inv`, `Circle.exp_intCast_mul`, `Real.Angle.toCircle_neg`, `PontryaginDual.map_apply`, `Real.fourierChar_apply'`, `Real.differentiable_fourierChar`, `Real.continuous_fourierChar`, `Circle.argPartialEquiv_target`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `ZMod.toCircle_intCast`, `ZMod.toCircle_natCast`, `Real.deriv_fourierChar`, `Complex.UnitDisc.instSMulCommClass_circle_closedBall`, `Real.differentiable_fourierChar_neg_bilinear_right`, `ZMod.injective_toCircle`, `Circle.coeHom_apply`, `rootsOfUnityCircleEquiv_apply`, `VectorFourier.fourierIntegral_comp_add_right`, `AddChar.zmod_zero`, `isLocalHomeomorph_circleExp`, `tendsto_integral_exp_inner_smul_cocompact`, `det_rotation`, `Fourier.fourierIntegral_def`, `Circle.expHom_apply`, `rotation_symm`, `Real.hasFDerivAt_fourierChar_neg_bilinear_right`, `ZMod.toCircle_apply`, `Circle.arg_exp`, `Real.differentiable_fourierChar_neg_bilinear_left`, `Circle.coe_exp`, `Circle.exp_zsmul`, `Circle.exp_eq_one`, `Circle.toUnits_apply`, `Real.fourierInv_eq`, `Real.probChar_apply`, `Circle.isCoveringMap_exp`, `AddChar.zmod_intCast`, `AddCircle.toCircle_nsmul`, `Circle.coe_zpow`, `VectorFourier.hasFDerivAt_fourierChar_smul`, `Real.fourierIntegral_real_eq`, `AddCircle.homeomorphCircle'_apply`, `AddCircle.homeomorphCircle_apply`, `AddChar.zmodAddEquiv_apply`, `Circle.exp_sub_two_pi`, `Circle.coe_div`, `Circle.argPartialEquiv_symm_apply`, `Circle.coe_one`, `AddChar.zmod_injective`, `Real.fourierIntegralInv_eq`, `Real.fderiv_fourierChar_neg_bilinear_left_apply`, `AddCircle.toCircle_neg`, `Fourier.fourierIntegral_comp_add_right`, `Circle.argEquiv_apply_coe`, `ZMod.rootsOfUnityAddChar_val`, `ZMod.toCircle_eq_circleExp`, `Circle.exp_nsmul`, `Complex.UnitDisc.coe_circle_smul`, `ZMod.stdAddChar_apply`, `Circle.argPartialEquiv_apply`, `MeasureTheory.charFun_eq_integral_probChar`, `Circle.norm_smul`, `contMDiff_circleExp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorph_circleExp` 📖	mathematical	—	`IsLocalHomeomorph` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Circle.exp`	—	`IsCoveringMap.isLocalHomeomorph` `Circle.isCoveringMap_exp`

---

← Back to Index