nat_mul_eq_of_eq_zero — Mathlib

English

If f is antiperiodic with c and f(0)=0, then f(n·c)=0 for all natural 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{N}, \ f(n\cdot c)=0$$$

Lean4

theorem nat_mul_eq_of_eq_zero [NonAssocSemiring α] [NegZeroClass β] (h : Antiperiodic f c) (hi : f 0 = 0) :
    ∀ n : ℕ, f (n * c) = 0
  | 0 => by rwa [Nat.cast_zero, zero_mul]
  | n + 1 => by simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

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