Def StarOrderedRing.ofNonnegIff

Modification history

2024-04-05 15:59

Mathlib/Algebra/Star/Order.lean

feat: make `StarOrderedRing` a mixin (#11872) …

Deleted StarOrderedRing.ofNonnegIff View on Github →

2023-06-08 07:32

Mathlib/Algebra/Star/Order.lean

chore: forward-port leanprover-community/mathlib#18854 (#4840) …

Added StarOrderedRing.ofNonnegIff View on Github →