exists_valuation_div_valuation_eq

English

For any γ in ValueGroupWithZero R, there exist a ∈ R and b ∈ posSubmonoid R such that valuation a / valuation b = γ.

Русский

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

LaTeX

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

Lean4

theorem exists_valuation_div_valuation_eq (γ : ValueGroupWithZero R) :
    ∃ (a : R) (b : posSubmonoid R), valuation _ a / valuation _ (b : R) = γ :=
  by
  induction γ using ValueGroupWithZero.ind with
  | mk a b
  use a, b
  simp [valuation, div_eq_mul_inv, ValueGroupWithZero.inv_mk (b : R) 1 b.prop]

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