[Merged by Bors] - chore: don't import algebra in Data.Multiset.Basic

[YaelDillies]

---

• depends on: [Merged by Bors] - refactor: unbundle Multiset.card #19777
• depends on: [Merged by Bors] - feat(List): count a (l₁.diff l₂) = count a l₁ - count a l₂ #19778
• depends on: [Merged by Bors] - chore(Data/Multiset/Basic): move the sub, union, inter sections lower #19863

[github-actions]

PR summary 6e707f4d64

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Multiset.Basic	371	358	-13 (-3.50%)

Import changes for all files

Files	Import difference
There are 3846 files with changed transitive imports taking up over 167185 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ add_assoc
+ add_comm
+ add_le_add_iff_left
+ add_le_add_iff_right
+ add_left_inj
+ add_right_inj
+ add_sub_assoc
+ add_sub_cancel
+ add_sub_cancel_right
+ add_zero
+ eq_sub_of_add_eq
+ instAddCancelCommMonoid
+ instAddLeftMono
+ instAddLeftReflectLE
+ instance : OrderedSub (Multiset α) where tsub_le_iff_right _n _m _k := Multiset.sub_le_iff_le_add
+ instance : Union (Multiset α)
+ le_add_sub
+ le_sub_add
+ sub_add_cancel
+ sub_add_eq_sub_sub
+ sub_le_iff_le_add'
+ sub_le_sub_right
+ zero_add
+ ⟨le_of_add_le_add_left,
+ ⟨le_of_add_le_add_right,
- instAddCommMonoid
- instance : AddLeftMono (Multiset α)
- instance : AddLeftReflectLE (Multiset α)
- instance : OrderedSub (Multiset α)
- instance : Union (Multiset α) := ⟨union⟩

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.01)

Current number	Change	Type
204	2	disabled simpNF lints

Current commit 6e707f4d64
Reference commit fceef13c1e

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-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor: unbundle Multiset.card #19777
• [Merged by Bors] - feat(List): count a (l₁.diff l₂) = count a l₁ - count a l₂ #19778
• [Merged by Bors] - chore(Data/Multiset/Basic): move the sub, union, inter sections lower #19863
  By Dependent Issues (🤖). Happy coding!

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style