int_mul_eq_of_eq_zero — Mathlib

English

If f is antiperiodic with c and f(0)=0, then f(n·c)=0 for every integer n.

Русский

Если f антипериодическая с периодом c и f(0)=0, тогда для каждого целого n выполняется f(n·c)=0.

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow f(0)=0 \rightarrow \forall n\in\mathbb{Z}, \ f(n\cdot c)=0$$$

Lean4

theorem int_mul_eq_of_eq_zero [NonAssocRing α] [SubtractionMonoid β] (h : Antiperiodic f c) (hi : f 0 = 0) :
    ∀ n : ℤ, f (n * c) = 0
  | (n : ℕ) => by rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
  | .negSucc n => by rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]

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