Theorem MonoidWithZeroHom.val_mrange_zero

Modification history

2025-09-29 16:14
Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean
feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom (#28329) …
Added MonoidWithZeroHom.val_mrange_zeroView on Github →