Commit 2025-08-15 07:37 77ee539f

View on Github →

feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (#27213)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean

added theorem ValuativeRel.IsDiscrete.of_compatible_withZeroMulInt

added theorem ValuativeRel.nonempty_orderIso_withZeroMul_int_iff