Theorem MonoidWithZeroHom.mrange_nontrivial

Modification history

2025-09-29 16:14
Mathlib/Algebra/GroupWithZero/Range.lean
feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom (#28329) …
Modified MonoidWithZeroHom.mrange_nontrivialView on Github →
2025-07-15 08:11
Mathlib/Algebra/GroupWithZero/Range.lean
feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial (#27114) …
Added MonoidWithZeroHom.mrange_nontrivialView on Github →