Def Subsemiring.nonneg

Modification history

2025-07-19 23:40
Mathlib/Algebra/Ring/Subsemiring/Order.lean
chore(Algebra/Ring/Subsemiring/Order): add missing projection (#27275) …
Modified Subsemiring.nonnegView on Github →
2025-04-10 16:38
Mathlib/Algebra/Ring/Subsemiring/Order.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified Subsemiring.nonnegView on Github →
2024-02-25 10:47
Mathlib/RingTheory/Subsemiring/Basic.lean
chore: split `Order`ed instances for subobjects into separate files (#10900) …
Modified Subsemiring.nonnegView on Github →
2024-02-13 21:51
Mathlib/RingTheory/Subsemiring/Basic.lean
feat: Submonoid of nonnegative elements (#10209) …
Added Subsemiring.nonnegView on Github →