toArithmeticFunction_congr — Mathlib

English

If f and f' agree for all n ≠ 0, then their corresponding arithmetic functions are equal after applying toArithmeticFunction.

Русский

Если f и f' совпадают при всех n ≠ 0, то их аппроксимации через toArithmeticFunction совпадают.

LaTeX

$$$\\forall f,f'\\; (\\forall n\\neq 0,\\; f(n)=f'(n)) \\Rightarrow \\operatorname{toArithmeticFunction}(f)=\\operatorname{toArithmeticFunction}(f').$$$

Lean4

theorem toArithmeticFunction_congr {R : Type*} [Zero R] {f f' : ℕ → R} (h : ∀ {n}, n ≠ 0 → f n = f' n) :
    toArithmeticFunction f = toArithmeticFunction f' := by
  ext
  simp_all [toArithmeticFunction]

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