structure DiscreteValuation (k : Type u_1) [Field k] : Type u_1

• val : Valuation k (WithZero (Multiplicative ℤ))
• val : Valuation k (WithZero (Multiplicative ℤ))
• val : Valuation k (WithZero (Multiplicative ℤ))
• surj : Function.Surjective ⇑self.val

@[implicit_reducible]

instance DiscreteValuation.instFunLikeWithZeroMultiplicativeInt {k : Type u_1} [Field k] : FunLike (DiscreteValuation k) k (WithZero (Multiplicative ℤ))

@[implicit_reducible]

instance DiscreteValuation.instCoeOutValuationWithZeroMultiplicativeInt {k : Type u_1} [Field k] : CoeOut (DiscreteValuation k) (Valuation k (WithZero (Multiplicative ℤ)))

noncomputable def discreteValuationAbsoluteValueFun {k : Type u_1} [Field k] (v : Valuation k (WithZero (Multiplicative ℤ))) {c : NNReal} (hc : c ≠ 0) (x : k) : NNReal

theorem isNonarchimedean_discreteValuationAbsoluteValueFun {k : Type u_1} [Field k] (v : Valuation k (WithZero (Multiplicative ℤ))) {c : NNReal} (hc : 1 < c) : IsNonarchimedean (discreteValuationAbsoluteValueFun v ⋯)

noncomputable def discreteValuationAbsoluteValue {k : Type u_1} [Field k] (v : Valuation k (WithZero (Multiplicative ℤ))) {c : NNReal} (hc : 1 < c) : AbsoluteValue k ℝ

theorem valuationRing_iff_forall_mem_or_inv_mem (A : Type u_1) [CommRing A] [IsDomain A] : ValuationRing A ↔ ∀ (x : FractionRing A), IsLocalization.IsInteger A x ∨ IsLocalization.IsInteger A x⁻¹