[Merged by Bors] - chore (Algebra.Order.Ring.Defs): split file and unbundle results

[mattrobball]

All of the theorems in Algebra.Order.Ring.Defs currently take bundled ordered algebraic typeclasses, eg OrderedSemiring as paramaters unecessarily. We unbundle the results keeping the algebra and order data/theorems separate and adding the mixin compatbility typeclasses as needed and place the theorems in Algebra.Order.Ring.Unbundled.Basic. As Algebra.Order.Ring.Defs and upstream resuls already allow us to pass from bundled classes to unbundled classes appropriately, we lose no uusability by doing this. We lessen dependecies and gain future flexibility.

---

• depends on [Merged by Bors] - chore (Algebra.Order.Monoid.Canonical.Defs): split off ExistsAddOfLE and ExistsMulOfLE #14390

[github-actions]

PR summary 99b3831c9d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Too many changes (2838)!

---

Declarations diff

+ instance : Monoid { x : R // 0 < x }
+ instance : One { x : R // 0 < x }
- instance [Nontrivial R] : Monoid { x : R // 0 < x }
- instance [Nontrivial R] : One { x : R // 0 < x }
- min_mul_min_le_mul_min_min

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>

[mattrobball]

Why is this fighting the blocked-by-other-pr label?!

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[YaelDillies]

Why is this fighting the blocked-by-other-pr label?!

Probably you had the syntax slightly wrong. I'm surprised this was merged without a

!bench

[mattrobball]

http://speed.lean-fro.org/mathlib4/run-detail/d4cc9472-dddb-4457-8316-df3d0425fded