Theorem ValuativeRel.IsDiscrete.of_compatible_withZeroMulInt

Modification history

2026-06-03 06:54
Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean
feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings (#36777) …
Modified ValuativeRel.IsDiscrete.of_compatible_withZeroMulIntView on Github →
2025-08-15 07:37
Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean
feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (#27213)
Added ValuativeRel.IsDiscrete.of_compatible_withZeroMulIntView on Github →