Commit 2023-10-23 14:19 e3421e31

View on Github →

feat: commutative star-ordered rings are ordered rings (#7309)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Ring/Star.lean

added def StarOrderedRing.toOrderedCommRing

added def StarOrderedRing.toOrderedCommSemiring