[Merged by Bors] - feat: Density of a finset

[YaelDillies]

The density of a finite set in an ambient group is a quantity of great interest in combinatorics.
This PR defines Finset.dens s for s : Finset α as the size of s divided by the size of α, with value in any semifield.
The API lemmas are copied from Finset.card (but not all Finset.card lemmas are sensible Finset.dens lemmas).

From LeanAPAP

---

[urkud]

See also commProb which you may want to port to the new definition. Also, do you plan to link it to the measure theory probability w.r.t. the uniform distribution?

[YaelDillies]

See also commProb which you may want to port to the new definition.

Nice observation! Will do so in a later PR.

do you plan to link it to the measure theory probability w.r.t. the uniform distribution?

Maybe in a distant future but right now I don't need it.

[github-actions]

PR summary 8241efc7a4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Positivity.Finset	488	538	+50 (+10.25%)

Import changes for all files

Files	Import difference
3 files Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Tactic	1
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite	6
Mathlib.Tactic.Positivity.Finset	50
Mathlib.Data.Finset.Density	537

---

Declarations diff

+ dens
+ dens_cons
+ dens_disjUnion
+ dens_empty
+ dens_eq_card_div_card
+ dens_eq_one
+ dens_eq_zero
+ dens_filter_add_dens_filter_not_eq_dens
+ dens_inter_add_dens_sdiff
+ dens_inter_add_dens_union
+ dens_le_dens
+ dens_le_dens_sdiff_add_dens
+ dens_lt_dens
+ dens_map_le
+ dens_mono
+ dens_ne_one
+ dens_ne_zero
+ dens_pos
+ dens_sdiff
+ dens_sdiff_add_dens
+ dens_sdiff_add_dens_eq_dens
+ dens_sdiff_add_dens_inter
+ dens_sdiff_comm
+ dens_singleton
+ dens_strictMono
+ dens_union_add_dens_inter
+ dens_union_le
+ dens_union_of_disjoint
+ dens_univ
+ evalFinsetDens
+ le_dens_sdiff
+ they
++ ⟨_,

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]

Feel free to put on the maintainer queue regardless of your response to my comment below, as long as you're convinced.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style