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.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iff {R : Type u_1} [Semiring R] [ValuativeRel R] : Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

@[deprecated ValuativeRel.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iff (since := "2026-09-08")]

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

Alias of ValuativeRel.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iff.

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