refactor(Algebra): generalise `support` from `Subsemiring` to `AddSubmonoid`

[artie2000]

• Generalise support(Add)Subgroup, support and HasIdealSupport from Subsemiring to (Add)Submonoid, moving the material to a new file
• Add documentation about supports
• Renamed declarations were not deprecated as the syntax for accessing them through dot notation remains identical

This PR is one in a series for unbundling RingCone and RingPreordering

---

[github-actions[bot]]

PR summary e9a7156e27

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Ring.Ordering.Basic	517	514	-3 (-0.58%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Order.Ring.Ordering.Basic	-3
Mathlib.Algebra.Order.Ring.Ordering.Defs	1
Mathlib.Algebra.Order.Support (new file)	310

---

Declarations diff

+ HasIdealSupport.neg_smul_mem + HasIdealSupport.smul_mem + coe_mulSupport + instHasIdealSupportToAddSubmonoidOfHasMemOrNegMem + instance (M : Subsemiring R) [HasMemOrNegMem M] : M.HasIdealSupport + instance (P : RingPreordering R) [HasMemOrNegMem P] : HasMemOrNegMem P.toSubsemiring + mem_mulSupport + mulSupport + toAddSubmonoid_support - coe_supportAddSubgroup - instance [HasMemOrNegMem P] : P.HasIdealSupport - mem_supportAddSubgroup - supportAddSubgroup - supportAddSubgroup_eq

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
1534	2	backwards compatibility flags
1487	2	privateInPublic flags

Current commit fd005d17f2 Reference commit e9a7156e27

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.