Lean4
/-- Construct a valuative relation on a ring using a valuation. -/
def ofValuation {S Γ : Type*} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : ValuativeRel S
where
rel x y := v x ≤ v y
rel_total x y := le_total (v x) (v y)
rel_trans := le_trans
rel_add hab hbc := (map_add_le_max v _ _).trans (sup_le hab hbc)
rel_mul_right _ h := by simp only [map_mul, mul_le_mul_right' h]
rel_mul_cancel h0
h := by
rw [map_zero, le_zero_iff] at h0
simp only [map_mul] at h
exact le_of_mul_le_mul_right h (lt_of_le_of_ne' zero_le' h0)
not_rel_one_zero := by simp