We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent e3ca552 commit 8f9fff7Copy full SHA for 8f9fff7
1 file changed
Mathlib/Analysis/Fourier/AddCircleMulti.lean
@@ -145,7 +145,7 @@ section Integral
145
146
variable (a : d → ℝ)
147
148
-/-- The measurable equivalence between `UnitAddTorus d` and a product of `Ioc` intervals. -/
+/-- The measurable equivalence between `UnitAddTorus d` and a product of `Ioc` intervals. -/
149
def measurableEquivPiIoc : UnitAddTorus d ≃ᵐ {x : d → ℝ | ∀ i, x i ∈ Ioc (a i) (a i + 1)} :=
150
(MeasurableEquiv.piCongrRight fun i => AddCircle.measurableEquivIoc 1 (a i)).trans <|
151
MeasurableEquiv.subtypePiEquivPi.symm
0 commit comments