Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring.positive_cone.one_pos

Modification history

2022-11-15 02:10
src/algebra/order/ring/cone.lean
refactor(algebra/order/ring): Make `strict_ordered_semiring`s nontrivial (#17394) …
Added ring.positive_cone.one_posView on Github →