Ring of integers under a given valuation #
The elements with valuation less than or equal to 1.
TODO: Define characteristic predicate.
Given a valuation v : R → Γ₀ and a ring homomorphism O →+* R, we say that O is the integers of v
if f is injective, and its range is exactly