Documentation Verification Report

Fourier

📁 Source: Mathlib/Analysis/Polynomial/Fourier.lean

Statistics

Metric	Count
Definitions `toAddCircle`	1
Theorems `fourierCoeff_toAddCircle`, `fourierCoeff_toAddCircle_eq_zero_of_lt_zero`, `fourierCoeff_toAddCircle_natCast`, `instTwoPiPos`, `sum_sq_norm_coeff_eq_circleAverage`, `integrable`, `toAddCircle_C_eq_smul_fourier_zero`, `toAddCircle_X_eq_fourier_one`, `toAddCircle_X_pow_eq_fourier`, `toAddCircle_monomial_eq_smul_fourier`	10
Total	11

Polynomial

Definitions

Name	Category	Theorems
`toAddCircle` 📖	CompOp	8 math math: `toAddCircle_X_pow_eq_fourier`, `toAddCircle.integrable`, `toAddCircle_monomial_eq_smul_fourier`, `fourierCoeff_toAddCircle_natCast`, `toAddCircle_X_eq_fourier_one`, `toAddCircle_C_eq_smul_fourier_zero`, `fourierCoeff_toAddCircle`, `fourierCoeff_toAddCircle_eq_zero_of_lt_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierCoeff_toAddCircle` 📖	mathematical	—	`fourierCoeff` `Real` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `instTwoPiPos` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DFunLike.coe` `ContinuousMap` `AddCircle` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMap.instFunLike` `AlgHom` `Polynomial` `Complex.instSemiring` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `coeff` `Complex.instZero`	—	`lt_or_ge` `induction_on'` `Nat.instAtLeastTwoHAddOfNat` `instTwoPiPos` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `fourierCoeff.congr_simp` `IsTopologicalSemiring.toContinuousAdd` `map_add` `SemilinearMapClass.toAddHomClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `fourierCoeff.add` `toAddCircle.integrable` `add_zero` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `coeff_add` `toAddCircle_monomial_eq_smul_fourier` `fourierCoeff.const_smul` `fourierCoeff_fourier` `Pi.single_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Int.instCharZero` `coeff_monomial`
`fourierCoeff_toAddCircle_eq_zero_of_lt_zero` 📖	mathematical	—	`fourierCoeff` `Real` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `instTwoPiPos` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DFunLike.coe` `ContinuousMap` `AddCircle` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMap.instFunLike` `AlgHom` `Polynomial` `Complex.instSemiring` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `Complex.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `instTwoPiPos` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `fourierCoeff_toAddCircle`
`fourierCoeff_toAddCircle_natCast` 📖	mathematical	—	`fourierCoeff` `Real` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `instTwoPiPos` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DFunLike.coe` `ContinuousMap` `AddCircle` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ContinuousMap.instFunLike` `AlgHom` `Polynomial` `Complex.instSemiring` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `coeff`	—	`Nat.instAtLeastTwoHAddOfNat` `instTwoPiPos` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `fourierCoeff_toAddCircle` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`
`instTwoPiPos` 📖	mathematical	—	`Fact` `Real` `Real.instLT` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.two_pi_pos`
`sum_sq_norm_coeff_eq_circleAverage` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `support` `Complex` `Complex.instSemiring` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `Complex.instNorm` `coeff` `Real.circleAverage` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `eval` `Complex.instZero` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `instTwoPiPos` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fact_one_le_two_ennreal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `QuotientAddGroup.borelSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `Real.instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `instIsTopologicalAddGroupReal` `Real.borelSpace` `AddSubgroup.normal_of_comm` `AddSubgroup.isClosed_of_discrete` `TopologicalSpace.t2Space_of_metrizableSpace` `Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `secondCountable_of_proper` `Complex.instProperSpace` `AddCircle.compactSpace` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `AddCircle.instIsProbabilityMeasureRealHaarAddCircle` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `tsum_sq_fourierCoeff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.integral_congr_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ContinuousMap.coeFn_toAEEqFun` `Filter.univ_mem'` `Nat.cast_injective` `Int.instCharZero` `Finset.sum_map` `Finset.sum_congr` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `le_or_gt` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Nat.instCharZero` `fourierCoeff_toAddCircle` `fourierCoeff_toLp` `AddCircle.integral_haarAddCircle` `Real.circleAverage.eq_1` `AddCircle.intervalIntegral_preimage` `mul_inv_rev` `AddCircle.scaled_exp_map_periodic` `div_self` `RCLike.charZero_rclike` `one_mul` `Function.Periodic.lift.congr_simp` `aeval_continuousMap_apply` `zero_add`
`toAddCircle_C_eq_smul_fourier_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Complex` `Polynomial` `Complex.instSemiring` `ContinuousMap` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `ContinuousMap.instSMul` `Algebra.toSMul` `CommSemiring.toSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `fourier`	—	`ContinuousMap.ext` `Nat.instAtLeastTwoHAddOfNat` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `aeval_C` `algebraMap_apply` `mul_one` `AddSubgroup.normal_of_comm` `zero_smul` `AddCircle.toCircle_zero`
`toAddCircle_X_eq_fourier_one` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Complex` `Polynomial` `Complex.instSemiring` `ContinuousMap` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `X` `fourier`	—	`ContinuousMap.ext` `Nat.instAtLeastTwoHAddOfNat` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `aeval_X` `AddSubgroup.normal_of_comm` `one_smul`
`toAddCircle_X_pow_eq_fourier` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Complex` `Polynomial` `Complex.instSemiring` `ContinuousMap` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `fourier`	—	`ContinuousMap.ext` `Nat.instAtLeastTwoHAddOfNat` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `aeval_X` `AddSubgroup.normal_of_comm` `natCast_zsmul` `AddCircle.toCircle_nsmul`
`toAddCircle_monomial_eq_smul_fourier` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Complex` `Polynomial` `Complex.instSemiring` `ContinuousMap` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instCommSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toAddCircle` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `ContinuousMap.instSMul` `Algebra.toSMul` `CommSemiring.toSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `fourier`	—	`ContinuousMap.ext` `Nat.instAtLeastTwoHAddOfNat` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `aeval_monomial` `algebraMap_apply` `mul_one` `AddSubgroup.normal_of_comm` `natCast_zsmul` `AddCircle.toCircle_nsmul`

Polynomial.toAddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable` 📖	mathematical	—	`MeasureTheory.Integrable` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `AddCircle` `Real` `Real.instAddCommGroup` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `QuotientAddGroup.measurableSpace` `AddCommGroup.toAddGroup` `Real.measurableSpace` `AddSubgroup.zmultiples` `DFunLike.coe` `ContinuousMap` `QuotientAddGroup.instTopologicalSpace` `Real.pseudoMetricSpace` `ContinuousMap.instFunLike` `AlgHom` `Polynomial` `Complex.instSemiring` `Complex.instCommSemiring` `Polynomial.semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Polynomial.algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `Polynomial.toAddCircle` `AddCircle.haarAddCircle` `Polynomial.instTwoPiPos`	—	`Nat.instAtLeastTwoHAddOfNat` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Polynomial.instTwoPiPos` `ContinuousOn.integrableOn_compact` `BorelSpace.opensMeasurable` `QuotientAddGroup.borelSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `Real.instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `instIsTopologicalAddGroupReal` `Real.borelSpace` `AddSubgroup.normal_of_comm` `AddSubgroup.isClosed_of_discrete` `TopologicalSpace.t2Space_of_metrizableSpace` `Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isCompact_univ` `AddCircle.compactSpace` `Continuous.continuousOn` `ContinuousMap.continuous`

---

← Back to Index