[Merged by Bors] - chore(Subring): don't import ordered ring classes for basic things

[mattrobball]

Having the ordered ring hierarchy results available here results in extra effort for typeclass searches.

---

• depends on: [Merged by Bors] - chore (Ring.Prod): move order instances on product rings #14122
• depends on: [Merged by Bors] - chore (Subgroup.Order): move ordered facts out of Basic and into Order #14121

[github-actions]

PR summary 354cd7883f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Submonoid.Membership	559	528	-31 (-5.55%)
Mathlib.Algebra.Ring.Subring.Basic	602	572	-30 (-4.98%)
Mathlib.Algebra.Module.Submodule.Ker	615	585	-30 (-4.88%)
Mathlib.Algebra.Module.Submodule.Range	616	586	-30 (-4.87%)

Import changes for all files

Files	Import difference
3 files Mathlib.GroupTheory.MonoidLocalization Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Algebra.Group.Submonoid.Membership	-31
38 files Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.LinearAlgebra.BilinearMap Mathlib.Algebra.Ring.Action.Invariant Mathlib.GroupTheory.Submonoid.Inverses Mathlib.LinearAlgebra.Span Mathlib.Algebra.Module.Submodule.Basic Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Data.DFinsupp.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Ring.Subring.Basic Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.Data.DFinsupp.NeLocus Mathlib.Algebra.DirectSum.Basic Mathlib.GroupTheory.Coprod.Basic Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.Algebra.Lie.Basic Mathlib.LinearAlgebra.Pi Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.Data.DFinsupp.Encodable Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Deprecated.Subring Mathlib.Data.DFinsupp.Notation Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Deprecated.Subfield Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Ker	-30
Mathlib.Algebra.BigOperators.Finsupp Mathlib.Algebra.BigOperators.Associated	-29
Mathlib.Algebra.Module.Submodule.Order	-27
Mathlib.Algebra.Ring.Subsemiring.Order	-24
Mathlib.GroupTheory.CoprodI	-10
4 files Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.DFinsupp.Lex Mathlib.Data.DFinsupp.Order	-4

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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>

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 87e3329.
There were significant changes against commit 7e4afad:

  Benchmark                                 Metric         Change
  ===============================================================
+ ~Mathlib.GroupTheory.MonoidLocalization   instructions   -14.9%

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore (Ring.Prod): move order instances on product rings #14122
• [Merged by Bors] - chore (Subgroup.Order): move ordered facts out of Basic and into Order #14121
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Thank you for continuing to comb mathlib's import yarn. If this is better for typeclass search, even nicer!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style