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.
- hom_inj : function.injective ⇑(algebra_map O R)
- map_le_one : ∀ (x : O), ⇑v (⇑(algebra_map O R) x) ≤ 1
- exists_of_le_one : ∀ ⦃r : R⦄, ⇑v r ≤ 1 → (∃ (x : O), ⇑(algebra_map O R) x = r)
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