English
Let hr ≠ 0 and h be the stated inequality. Then for every x, if v(x) ≠ 0, one has v(x) = 1.
Русский
Если hr ≠ 0 и выполняется требование h, то для любого x с v(x) ≠ 0 имеет место v(x) = 1.
LaTeX
$$$hr \neq 0 \Rightarrow (\forall x: K, v(x) \neq 0 \Rightarrow v(x)=1)$$$
Lean4
theorem map_eq_one_of_forall_lt [MulArchimedean Γ₀] {v : Valuation K Γ₀} {r : Γ₀} (hr : r ≠ 0)
(h : ∀ x : K, v x ≠ 0 → r < v x) (x : K) (hx : v x ≠ 0) : v x = 1 :=
by
lift r to Γ₀ˣ using IsUnit.mk0 _ hr
rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H
· obtain ⟨k, hk⟩ := exists_pow_lt H r
specialize h (x ^ k) (by simp [hx])
simp [← Units.val_lt_val, ← map_pow, h.not_gt] at hk
· simpa [Units.ext_iff] using H
· rw [← inv_lt_one'] at H
obtain ⟨k, hk⟩ := exists_pow_lt H r
specialize h (x ^ (-k : ℤ)) (by simp [hx])
simp only [zpow_neg, zpow_natCast, map_inv₀, map_pow] at h
simp [← Units.val_lt_val, h.not_gt, inv_pow] at hk
