[Merged by Bors] - chore: delay imports of Star

[kim-em]

No description provided.

[github-actions]

PR summary a9a992889b

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Star.Basic	493	394	-99 (-20.08%)
Mathlib.Algebra.Module.LinearMap.Basic	515	498	-17 (-3.30%)
Mathlib.Algebra.Module.Equiv	518	501	-17 (-3.28%)
Mathlib.Algebra.Algebra.Defs	612	609	-3 (-0.49%)
Mathlib.Analysis.Seminorm	1147	1143	-4 (-0.35%)
Mathlib.Algebra.RingQuot	874	871	-3 (-0.34%)
Mathlib.Topology.Algebra.Module.Basic	964	961	-3 (-0.31%)
Mathlib.Algebra.Algebra.Equiv	731	729	-2 (-0.27%)
Mathlib.Analysis.Normed.Order.UpperLower	1162	1159	-3 (-0.26%)
Mathlib.Analysis.Normed.Group.Quotient	1169	1166	-3 (-0.26%)
Mathlib.Data.Real.Sqrt	1033	1031	-2 (-0.19%)
Mathlib.Analysis.SumOverResidueClass	1123	1121	-2 (-0.18%)

---

Declarations diff

+ Real.instStarOrderedRing
- instance : StarOrderedRing ℝ

You can run this locally as follows

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

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

[Ruben-VandeVelde]

Have you considered going the other way? It seems like we could have a Star.Defs file could be very light-weight.

Also please keep the imports sorted

[kim-em]

Have you considered going the other way? It seems like we could have a Star.Defs file could be very light-weight.

We should do that too! :-)

[kim-em]

Also please keep the imports sorted

I'm assuming the rule is just alphabetic? I hadn't realised we were doing this.

[kim-em]

(The motivation here was being annoyed at encountering these imports when doing a minimization.)

[mattrobball]

bors delegate+

[mathlib-bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kim-em]

bors merge

[eric-wieser]

bors r-

bors d+

[mathlib-bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors]

Canceled.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style