Theorem ValuativeRel.nonempty_orderIso_withZeroMul_int_iff

Modification history

2026-09-24 13:25
Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean
chore(RingTheory/Valuation/DiscreteValuativeRel): fix two typos in lemma name (#43587)
Deleted ValuativeRel.nonempty_orderIso_withZeroMul_int_iffView on Github →
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_iffView 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_iffView on Github →