angle): more 2π = 0 lemmas (#11482)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lemmas (#11482) Add some more lemmas useful for manipulation of `real.angle` expressions.

Author

jsm28

Parents

ed57bdd3

mathlib3 f4b93c8c - feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lemmas (#11482)

mathlib3
f4b93c8c - feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lemmas (#11482)