Ring of integers under a given valuation #
The elements with valuation less than or equal to 1.
TODO: Define characteristic predicate.
The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.
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