Commit 2025-07-19 23:40 e9b079d0

View on Github →

chore(Algebra/Ring/Subsemiring/Order): add missing projection (#27275) Add standard simp projection Subsemiring.mem_nonneg

Estimated changes

added theorem Subsemiring.mem_nonneg
modified def Subsemiring.nonneg