Theorems · Definition · general topology
UnitAddTorus
Type u_1 → Type u_1
The product indexed by d of copies of the unit circle.
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- UnitAddCircleproof · cited by 157
Cited by35
Results whose statement or proof uses this declaration.
- UnitAddTorus.mFourierstatement and proof · cited by 15
- UnitAddTorus.mFourierCoeffstatement and proof · cited by 8
- UnitAddTorus.mFourierLpstatement · cited by 8
- UnitAddTorus.measurableEquivPiIocstatement · cited by 7
- UnitAddTorus.mFourierBasisstatement · cited by 4
- UnitAddTorus.mFourierSubalgebrastatement and proof · cited by 3
- UnitAddTorus.measurePreserving_equivPiIocstatement and proof · cited by 2
- UnitAddTorus.coeFn_mFourierLpstatement · cited by 1
- UnitAddTorus.coe_mFourierBasisstatement · cited by 1
- UnitAddTorus.hasSum_mFourier_series_L2statement and proof · cited by 1
- UnitAddTorus.hasSum_mFourier_series_of_summablestatement and proof · cited by 1
- UnitAddTorus.hasSum_prod_mFourierCoeffstatement and proof · cited by 1