# Ring of integers under a given valuation #

The elements with valuation less than or equal to 1.

TODO: Define characteristic predicate.

def Valuation.integer {R : Type u} {Γ₀ : Type v} [Ring R] (v : Valuation R Γ₀) :

The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.

Equations
• v.integer = { carrier := {x : R | v x 1}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := }
Instances For
theorem Valuation.mem_integer_iff {R : Type u} {Γ₀ : Type v} [Ring R] (v : Valuation R Γ₀) (r : R) :
r v.integer v r 1
structure Valuation.Integers {R : Type u} {Γ₀ : Type v} [] (v : Valuation R Γ₀) (O : Type w) [] [Algebra O 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 v.integer.

• hom_inj : Function.Injective ()
• map_le_one : ∀ (x : O), v (() x) 1
• exists_of_le_one : ∀ ⦃r : R⦄, v r 1∃ (x : O), () x = r
Instances For
theorem Valuation.Integers.hom_inj {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (self : v.Integers O) :
theorem Valuation.Integers.map_le_one {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (self : v.Integers O) (x : O) :
v (() x) 1
theorem Valuation.Integers.exists_of_le_one {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (self : v.Integers O) ⦃r : R :
v r 1∃ (x : O), () x = r
instance Valuation.instAlgebraSubtypeMemSubringInteger {R : Type u} {Γ₀ : Type v} [] (v : Valuation R Γ₀) :
Algebra (v.integer) R
Equations
theorem Valuation.integer.integers {R : Type u} {Γ₀ : Type v} [] (v : Valuation R Γ₀) :
v.Integers v.integer
theorem Valuation.Integers.one_of_isUnit' {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] {x : O} (hx : ) (H : ∀ (x : O), v (() x) 1) :
v (() x) = 1
theorem Valuation.Integers.one_of_isUnit {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (hv : v.Integers O) {x : O} (hx : ) :
v (() x) = 1
theorem Valuation.Integers.isUnit_of_one {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (hv : v.Integers O) {x : O} (hx : IsUnit (() x)) (hvx : v (() x) = 1) :
theorem Valuation.Integers.le_of_dvd {R : Type u} {Γ₀ : Type v} [] {v : Valuation R Γ₀} {O : Type w} [] [Algebra O R] (hv : v.Integers O) {x : O} {y : O} (h : x y) :
v (() y) v (() x)
theorem Valuation.Integers.dvd_of_le {F : Type u} {Γ₀ : Type v} [] {v : Valuation F Γ₀} {O : Type w} [] [Algebra O F] (hv : v.Integers O) {x : O} {y : O} (h : v (() x) v (() y)) :
y x
theorem Valuation.Integers.dvd_iff_le {F : Type u} {Γ₀ : Type v} [] {v : Valuation F Γ₀} {O : Type w} [] [Algebra O F] (hv : v.Integers O) {x : O} {y : O} :
x y v (() y) v (() x)
theorem Valuation.Integers.le_iff_dvd {F : Type u} {Γ₀ : Type v} [] {v : Valuation F Γ₀} {O : Type w} [] [Algebra O F] (hv : v.Integers O) {x : O} {y : O} :
v (() x) v (() y) y x