We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent cd08df5 commit e3ca552Copy full SHA for e3ca552
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