Commit 2026-09-01 11:45 7555c35e

feat(Algebra/Order/Nonneg): add Nonneg for nonnegative subtype (#41134) Currently the nonnegative subtype is denoted {x : R // 0 ≤ x} which has a tendency to be used inconsistently and does not print well. This PR introduces

/- The subtype of nonnegative elements. -/
abbrev Nonneg (α : Type*) [Zero α] [LE α] := { x : α // 0 ≤ x }

and replaces {x : R // 0 ≤ x} by Nonneg R throughout mathlib. In the longer term, Nonneg could be converted to a one-field or two-field structure, as discussed on Zulip: #general > backward.isDefEq.respectTransparency @ 💬. This PR is the first step in this direction, by introducing the name Nonneg throughout mathlib.