Theorems · Definition · harmonic analysis
Polynomial.toAddCircle
Polynomial ℂ →ₐ[ℂ] C(AddCircle (2 * Real.pi), ℂ)
Algebra map from ℂ[X] to C(AddCircle (2 * π), ℂ) that evaluates polynomials on the unit
circle. For a polynomial p, this maps it to the function fun θ ↦ p (exp (I * θ)).
- Defined in
- Mathlib.Analysis.Polynomial.Fourier
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Polynomialstatement · cited by 5,681
- Complexstatement · cited by 5,565
- AlgHomstatement · cited by 3,236
- ContinuousMapstatement · cited by 2,491
- Real.pistatement and proof · cited by 1,774
- Polynomial.aevalproof · cited by 615
- AddSubgroup.zmultiplesstatement · cited by 493
- AddCirclestatement and proof · cited by 189
- AddCircle.toCircleproof · cited by 41
Cited by9
Results whose statement or proof uses this declaration.
- Polynomial.fourierCoeff_toAddCirclestatement and proof · cited by 3
- Polynomial.sum_sq_norm_coeff_eq_circleAverageproof · cited by 1
- Polynomial.toAddCircle.integrablestatement and proof · cited by 1
- Polynomial.toAddCircle_monomial_eq_smul_fourierstatement · cited by 1
- Polynomial.toAddCircle_X_pow_eq_fourierstatement · cited by 0
- Polynomial.toAddCircle_C_eq_smul_fourier_zerostatement · cited by 0
- Polynomial.toAddCircle_X_eq_fourier_onestatement · cited by 0
- Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zerostatement · cited by 0
- Polynomial.fourierCoeff_toAddCircle_natCaststatement · cited by 0