nat_mul_eq — Mathlib

English

Let f be periodic with period c in a NonAssocSemiring α. Then for all natural n, f(n·c) = f(0).

Русский

Пусть f периодична с периодом c в NonAssocSemiring α. Тогда для каждого натурального n выполняется f(n·c) = f(0).

LaTeX

$$$[NonAssocSemiring\ α]\Rightarrow(\forall h:Periodic\ f\ c)(\forall n\in \mathbb{N})\, f(n\cdot c)=f(0).$$$

Lean4

theorem nat_mul_eq [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : f (n * c) = f 0 :=
  (h.nat_mul n).eq

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