Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-15 08:26 dbd468d9

View on Github →

feat(analysis/special_functions/trigonometric): periodicity of sine, cosine (#7107) Previously we only had sin (x + 2 * π) = sin x and cos (x + 2 * π) = cos x. I extend those results to cover shifts by any integer multiple of 2 * π, not just 2 * π. I also provide corresponding sub lemmas.

Estimated changes