embed_strictMono — Mathlib

English

For any γ ∈ ValueGroupWithZero R, there exist a,b ∈ R with valuation a / valuation b = γ.

Русский

Для любого γ ∈ ValueGroupWithZero R существуют a,b ∈ R такие, что valuation a / valuation b = γ.

LaTeX

$$$\\exists a,b \\in R, \\; \\dfrac{\\mathrm{valuation}(a)}{\\mathrm{valuation}(b)} = \\gamma$$$

Lean4

theorem embed_strictMono [v.Compatible] : StrictMono (embed v) :=
  by
  intro a b h
  obtain ⟨a, r, rfl⟩ := exists_valuation_div_valuation_eq a
  obtain ⟨b, s, rfl⟩ := exists_valuation_div_valuation_eq b
  simp only [map_div₀]
  rw [div_lt_div_iff₀] at h ⊢
  any_goals simp [zero_lt_iff]
  rw [← map_mul, ← map_mul, (isEquiv (valuation R) v).lt_iff_lt] at h
  simpa [embed] using h

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