# Commit2024-04-02 13:07a3021aec

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`