angle): `coe_pi_add_coe_pi` (#12064)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/angle): `coe_pi_add_coe_pi` (#12064) Add another `simp` lemma to those expressing in different ways that 2π is zero as a `real.angle`.

Author

jsm28

Parents

daf2989a

mathlib 06e6b35d - feat(analysis/special_functions/trigonometric/angle): `coe_pi_add_coe_pi` (#12064)

mathlib
06e6b35d - feat(analysis/special_functions/trigonometric/angle): `coe_pi_add_coe_pi` (#12064)