mathlib3

2bb25f05 - feat(algebra/periodic): lifting to function on quotient group (#11321)

feat(algebra/periodic): lifting to function on quotient group (#11321) I want to make more use of the type `real.angle` in `analysis.special_functions.trigonometric.angle`, including defining functions from this type in terms of periodic functions from `ℝ`. To support defining such functions, add a definition `periodic.lift` that lifts a periodic function from `α` to a function from `α ⧸ (add_subgroup.zmultiples c)`, along with a lemma `periodic.lift_coe` about the values of the resulting function.