add_nsmul_eq — Mathlib

English

For AddMonoid α and SubtractionMonoid β, if f is Antiperiodic with c, then for natural n we have f(x + n•c) = (-1)^n f(x).

Русский

Для AddMonoid α и SubtractionMonoid β, если f антипериодическая с c, тогда при любом натуральном n выполняется f(x + n•c) = (-1)^n f(x).

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \forall n \in \mathbb{N}, \ f(x + n\cdot c) = (-1)^n \cdot f(x)$$$

Lean4

theorem add_nsmul_eq [AddMonoid α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) :
    f (x + n • c) = (-1) ^ n • f x :=
  by
  rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_nsmul_periodic]
    simp
  · rw [h.odd_nsmul_antiperiodic]
    simp [pow_add]

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