nat_odd_mul_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).

LaTeX

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

Lean4

theorem nat_odd_mul_antiperiodic [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) :
    Antiperiodic f (n * (2 * c) + c) := fun x => by rw [← add_assoc, h, h.nat_even_mul_periodic]

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