ext — Mathlib

English

Two arithmetic functions are equal iff they agree pointwise on natural numbers.

Русский

Две арифметические функции равны тогда и только тогда, когда они совпадают на всех натуральных аргументах.

LaTeX

$$$\\forall \\{f,g : ArithmeticFunction R\\}, (\\forall x, f(x) = g(x)) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem ext ⦃f g : ArithmeticFunction R⦄ (h : ∀ x, f x = g x) : f = g :=
  ZeroHom.ext h

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