odd_nsmul_antiperiodic — Mathlib

English

For a semiring α and β with involutive negation, if f is antiperiodic with c, then f is antiperiodic with (2·n+1)·c for any n ∈ ℕ.

Русский

Для полускольа α и β с инволютивным отрицанием, если f антипериодична с c, то она антипериодична с (2n+1)·c для любого n ∈ ℕ.

LaTeX

$$$[NonAssocSemiring\ α][InvolutiveNeg\ β]\Rightarrow (h:Antiperiodic\ f\ c)\Rightarrow \forall n\in \mathbb{N}, Antiperiodic\ f\ ((2\cdot n+1)\cdot c).$$$

Lean4

theorem odd_nsmul_antiperiodic [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) :
    Antiperiodic f ((2 * n + 1) • c) := fun x => by rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Похожие утверждения