# Commit 2024-04-02 13:07 a3021aec

View on Github →feat: value of f (x + n * c), where f is antiperiodic with antiperiod c (#11436)
Add `@[simp]`

theorem `negOnePow_two_mul_add_one`

to `Algebra.GroupPower.NegOnePow`

, which states that `(2 * n + 1).negOnePow = -1`

.
Add theorems to `Algebra.Periodic`

about the value of `f (x + n • c)`

, `f (x - n • c)`

, and `f (n • c - x)`

, where we have `Antiperiodic f c`

. All these theorems have variants for either `n : ℕ`

or `n : ℤ`

, and they also have variants using `*`

instead of `•`

if the domain and codomain of `f`

are rings.
For all real numbers `x`

and all integers `n`

. deduce the following. All these theorems are in `Analysis.SpecialFunctions.Trigonometric.Basic`

, they are not `@[simp]`

, and they have a variation (using the notation `(-1) ^ n`

instead of `n.negOnePow`

) for natural number `n`

.

`sin (x + n * π) = n.negOnePow * sin x`

`sin (x - n * π) = n.negOnePow * sin x`

`sin (n * π - x) = -(n.negOnePow * sin x)`

`cos (x + n * π) = n.negOnePow * cos x`

`cos (x - n * π) = n.negOnePow * cos x`

`cos (n * π - x) = n.negOnePow * cos x`