Commit 2025-09-29 16:14 ee6d62f1

View on Github →

feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom (#28329) Before, they were only for Valuation, but that is too restricted

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupWithZero/Range.lean

modified theorem MonoidWithZeroHom.mrange_nontrivial

modified theorem MonoidWithZeroHom.range_nontrivial

Created Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean

added theorem MonoidWithZeroHom.val_mrange_zero

Modified Mathlib/RingTheory/Valuation/Archimedean.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

modified theorem Valuation.val_mrange_zero