Skip to content

Commit bf42c2f

Browse files
CoolRmalEtienneC30
andauthored
Update Mathlib/Analysis/Fourier/AddCircleMulti.lean
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
1 parent 8f9fff7 commit bf42c2f

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Analysis/Fourier/AddCircleMulti.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,7 @@ def measurableEquivPiIoc : UnitAddTorus d ≃ᵐ {x : d → ℝ | ∀ i, x i ∈
151151
MeasurableEquiv.subtypePiEquivPi.symm
152152

153153
/-- The measurable equivalence between `UnitAddTorus d` and a product of `Ico` intervals. -/
154-
def measurableEquivPiIco : UnitAddTorus d ≃ᵐ {x : d → ℝ | ∀ i, x i ∈ Ico (a i) (a i + 1)} :=
154+
def measurableEquivPiIco : UnitAddTorus d ≃ᵐ {x : d → ℝ | ∀ i, x i ∈ Ico (a i) (a i + 1)} :=
155155
(MeasurableEquiv.piCongrRight fun i => AddCircle.measurableEquivIco 1 (a i)).trans <|
156156
MeasurableEquiv.subtypePiEquivPi.symm
157157

0 commit comments

Comments
 (0)