Valuation.Integers.dvd_of_le

theorem Valuation.Integers.dvd_of_le : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F], v.Integers O → ∀ {x y : O}, v ((algebraMap O F) x) ≤ v ((algebraMap O F) y) → y ∣ x

The theorem `Valuation.Integers.dvd_of_le` states that for any Field `F`, any Linear Ordered Commutative Group With Zero `Γ₀`, any Valuation `v` of `F` with values in `Γ₀`, any Commutative Ring `O`, and any Algebra structure of `O` over `F`, if `O` is the ring of integers in `F` with respect to `v`, then for any elements `x` and `y` in `O`, if the valuation of the image of `x` under the algebra structure map from `O` to `F` is less than or equal to the valuation of the image of `y` under the same map, then `y` divides `x`. In mathematical terms, it asserts that if $v(\phi(x)) \leq v(\phi(y))$ for $x, y \in O$ where $\phi: O \to F$ is the algebra structure map, then $y$ divides $x$ in the ring `O`.

More concisely: If `v` is a valuation of a field `F` with values in a linearly ordered commutative group `Γ₀`, and `O` is the ring of integers in `F` with respect to `v`, then for all `x, y ∈ O`, `y` divides `x` in `O` if and only if the valuation of `x` under the algebra structure map is less than or equal to the valuation of `y` under the same map.