chore: Move UnitAddTorus to Topology/Instances/AddCircle/Real.lean (#39452)

Previous location of `UnitAddTorus` in Analysis/Fourier/AddCircleMulti.lean was ad-hoc and required users to import the entire Fourier analysis infrastructure just to use the torus. I suggest moving it to it's natural home beside `UnitAddCircle`.

Author: Deicyde

Mathlib/Analysis/Fourier/AddCircleMulti.lean

@@ -37,9 +37,6 @@ local instance : Measure.IsAddHaarMeasure (volume : Measure UnitAddCircle) :=
 local instance : IsProbabilityMeasure (volume : Measure UnitAddCircle) :=
   inferInstanceAs (IsProbabilityMeasure AddCircle.haarAddCircle)
 
-/-- The product of finitely many copies of the unit circle, indexed by `d`. -/
-abbrev UnitAddTorus (d : Type*) := d → UnitAddCircle
-
 namespace UnitAddTorus
 
 variable {d : Type*} [Fintype d]

Mathlib/Topology/Instances/AddCircle/Real.lean

@@ -48,6 +48,9 @@ section UnitAddCircle
 abbrev UnitAddCircle :=
   AddCircle (1 : ℝ)
 
+/-- The product indexed by `d` of copies of the unit circle. -/
+abbrev UnitAddTorus (d : Type*) := d → UnitAddCircle
+
 end UnitAddCircle
 
 namespace ZMod