English
For an additive group α and a SubtractionMonoid β, if f is Antiperiodic with c, then f(x + n•c) = (n.negOnePow)•f x for all integers n.
Русский
Для группы дополнения α и моноида β, если f антипериодическая с c, то при любом целочисленном n выполняется f(x + n•c) = (-1)^n f(x).
LaTeX
$$$\text{Antiperiodic}(f,c) \rightarrow \forall x, \forall n\in\mathbb{Z}, \ f(x+n\cdot c) = (n.negOnePow) \cdot f(x)$$$
Lean4
theorem add_zsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) :
f (x + n • c) = (n.negOnePow : ℤ) • f x :=
by
rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
· rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
· rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg, Units.val_one, neg_zsmul, one_zsmul]
