Commit 2024-04-08 15:44 d8c86746

View on Github →

refactor: Move AddCircle.toCircle to earlier file (#12000) This PR moves AddCircle.toCircle to the earlier file Analysis/SpecialFunctions/Complex/Circle since AddCircle.toCircle only depends on periodic_expMapCircle and not the heavy imports of Analysis/Fourier/AddCircle.

Estimated changes

Modified Mathlib/Analysis/Fourier/AddCircle.lean

deleted theorem AddCircle.continuous_toCircle

deleted theorem AddCircle.injective_toCircle

deleted theorem AddCircle.scaled_exp_map_periodic

deleted def AddCircle.toCircle

deleted theorem AddCircle.toCircle_add

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem AddCircle.continuous_toCircle

added theorem AddCircle.injective_toCircle

added theorem AddCircle.scaled_exp_map_periodic

added theorem AddCircle.toCircle_add