exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq

English

For γ in (ValueGroupWithZero R)ˣ, there exist a,b ∈ posSubmonoid R such that valuation a / valuation b = γ.

Русский

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

LaTeX

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

Lean4

theorem exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq (γ : (ValueGroupWithZero R)ˣ) :
    ∃ (a b : posSubmonoid R), valuation R a / valuation _ (b : R) = γ :=
  by
  obtain ⟨a, b, hab⟩ := exists_valuation_div_valuation_eq γ.val
  lift a to posSubmonoid R using by
    contrapose! hab
    rw [posSubmonoid_def, not_srel_iff, ← valuation_eq_zero_iff] at hab
    simp [hab, eq_comm]
  use a, b

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