Def StarOrderedRing.ofLEIff

Modification history

2024-04-05 15:59
Mathlib/Algebra/Star/Order.lean
feat: make `StarOrderedRing` a mixin (#11872) …
Deleted StarOrderedRing.ofLEIffView on Github →
2023-09-14 06:57
Mathlib/Algebra/Star/Order.lean
chore: tidy various files (#7137)
Added StarOrderedRing.ofLEIffView on Github →