[Merged by Bors] - refactor(Algebra/Star/Order): Use NonUnitalStarRingHom in Algebra.Star.Order#13089
Closed
mans0954 wants to merge 48 commits intomasterfrom mans0954/StarRingEquivClass.instOrderIsoClass
Commits
Commits on May 15, 2024
- committed
- committed
- committed
- committed
Commits on May 19, 2024
Commits on May 20, 2024
- committed
- committed
Commits on May 21, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
Commits on May 22, 2024
- committed
- committed
- committed
- committed
- committed
- committed
Commits on May 25, 2024
Commits on May 27, 2024
- committed
- committed
- committed