angle): rfl lemmas for nat and int smul actions on angle (#15003)

Commit

3 years ago

chore(analysis/special_functions/trigonometric/angle): rfl lemmas for nat and int smul actions on angle (#15003) These can't be simp, because the simp-normal form is multiplication.

Author

eric-wieser

Parents

37bf8a2e

mathlib cf4d987d - chore(analysis/special_functions/trigonometric/angle): rfl lemmas for nat and int smul actions on angle (#15003)

mathlib
cf4d987d - chore(analysis/special_functions/trigonometric/angle): rfl lemmas for nat and int smul actions on angle (#15003)