eq_on_nat_iff_eq — Mathlib

English

Two absolute values on Q are equal iff their values agree on all natural numbers.

Русский

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

LaTeX

$$$(\\forall n \\in \\mathbb{N}, f(n) = g(n)) \\Leftrightarrow f = g$$$

Lean4

/-- Values of an absolute value on the rationals are determined by the values on the natural
numbers. -/
theorem eq_on_nat_iff_eq : (∀ n : ℕ, f n = g n) ↔ f = g :=
  by
  refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩
  ext1 z
  rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]

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