refactor(Algebra/Star/Order): Use NonUnitalStarRingHom in Algebra.Star.Order

[mans0954]

trafficstars

Refactor Algebra.Star.Order to use the new non-unital *-ring homomorphisms / isomorphisms introduced in #12924

---

• [x] depends on: #12924

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary 809384e3dd

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Star.Order	507	508	+1 (+0.20%)

Import changes for all files

Files

Import difference

24 files Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Data.Complex.Exponential Mathlib.Algebra.Order.Ring.Star Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Data.Matrix.Rank Mathlib.Data.Rat.Star Mathlib.Algebra.Star.CHSH Mathlib.Algebra.Star.Order Mathlib.Data.Int.Star Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Data.Real.StarOrdered Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.CPolynomial Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.Polynomial

1

---

Declarations diff

+ NonUnitalStarRingHom.map_le_map_of_map_star + instance (priority := 100) StarRingEquivClass.instOrderIsoClass [EquivLike F R S] + instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S] - NonUnitalRingHom.map_le_map_of_map_star - instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S] [StarHomClass F R S] - instance (priority := 100) StarRingHomClass.instOrderIsoClass [EquivLike F R S] [StarHomClass F R S]

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12924~~ By Dependent Issues (🤖). Happy coding!

[mans0954]

@riccardobrasca I assume you added the WIP label because I previously forgot to tag this with the now-defunct awaiting-review label rather than because you thought some further work was needed?

[riccardobrasca]

@riccardobrasca I assume you added the WIP label because I previously forgot to tag this with the now-defunct awaiting-review label rather than because you thought some further work was needed?

Yes, feel free to remove it if it's ready for reviews.

[kim-em]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style