Commit 2025-07-15 08:11 4627273f
View on Github →feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial (#27114) for proving that it is not densely ordered for PIR -> DVR for valuations Since this is a nontrivial set, then it can't be densely ordered when the codomain is Zm0, as shown in #27112. Together, it is used in #27117 to show that a Zm0-valued valuation's subring is a DVR.