mathlib
01adfd65 - chore(analysis/special_functions): add some `@[simp]` attrs (#9423)

Commit

4 years ago

chore(analysis/special_functions): add some `@[simp]` attrs (#9423) Add `@[simp]` attrs to `real.sin_add_pi` and similar lemmas.

Author

urkud

Parents