Theorem ValuativeRel.nonempty_orderIso_withZeroMul_int_iff

Modification history

2026-06-03 06:54

Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean

feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings (#36777) …

Modified ValuativeRel.nonempty_orderIso_withZeroMul_int_iff View 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.nonempty_orderIso_withZeroMul_int_iff View on Github →