Theorem Valuation.val_mrange_zero

Modification history

2025-09-29 16:14
Mathlib/RingTheory/Valuation/Basic.lean
feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom (#28329) …
Modified Valuation.val_mrange_zeroView on Github →
2025-01-14 16:01
Mathlib/RingTheory/Valuation/Basic.lean
feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered (#16619)
Added Valuation.val_mrange_zeroView on Github →