Theorem RingCone.coe_nonneg

Modification history

2026-10-29 02:16

Mathlib/Algebra/Order/Ring/Cone.lean

refactor(Algebra/Order): unbundle group and ring cone (#37298) …

Modified RingCone.coe_nonneg View on Github →

2024-09-05 15:25

Mathlib/Algebra/Order/Ring/Cone.lean

feat(Algebra/Order): rewrite positive cones to use substructure pattern (#15975) …

Added RingCone.coe_nonneg View on Github →