const_equiv — Mathlib

English

The constant padic-norm sequences detect equality of rationals: const(pad icNorm p)(q) ≈ const(pad icNorm p)(r) iff q = r.

Русский

Постоянные последовательности нормы p-адического типа различают рациональные числа: const(padicNorm p)(q) ≈ const(padicNorm p)(r) эквивалентно q = r.

LaTeX

$$$\\operatorname{const}(\\mathrm{padicNorm}_p)(q) \\approx \\operatorname{const}(\\mathrm{padicNorm}_p)(r) \\iff q = r$$$

Lean4

theorem const_equiv {q r : ℚ} : const (padicNorm p) q ≈ const (padicNorm p) r ↔ q = r :=
  ⟨fun heq ↦ eq_of_sub_eq_zero <| const_limZero.1 heq, fun heq ↦ by rw [heq]⟩

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