Theorem ValuativeRel.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iff

Modification history

2026-09-24 13:25
Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean
chore(RingTheory/Valuation/DiscreteValuativeRel): fix two typos in lemma name (#43587)
Added ValuativeRel.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iffView on Github →