Discrete Valuative Relations

Discrete valuative relations have a maximal element less than one in the value group.

In the rank-one case, this is equivalent to the value group being isomorphic to ℤᵐ⁰.

theorem ValuativeRel.nonempty_orderIso_withZeroMul_int_iff {R : Type u_1} [CommRing R] [ValuativeRel R] : Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

theorem ValuativeRel.IsDiscrete.of_compatible_withZeroMulInt {R : Type u_1} [CommRing R] [ValuativeRel R] (v : Valuation R (WithZero (Multiplicative ℤ))) [v.Compatible] : IsDiscrete R