[Merged by Bors] - feat: cardinality of Hahn series

[vihdzp]

This is a very preliminary development; most of the PR is really just lemmas about HahnSeries.support. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual.

---

[github-actions]

PR summary 4d33172004

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.HahnSeries.Cardinal (new file)	855

---

Declarations diff

+ cardSupp
+ cardSupp_add_le
+ cardSupp_congr
+ cardSupp_map_le
+ cardSupp_mono
+ cardSupp_mul_le
+ cardSupp_neg
+ cardSupp_neg_le
+ cardSupp_single_le
+ cardSupp_single_of_ne
+ cardSupp_smul_le
+ cardSupp_sub_le
+ cardSupp_truncLT_le
+ cardSupp_zero
+ support_map_subset
+ support_mk
+ support_mul_subset
+ support_neg_subset
+ support_smul_subset
+ support_sub_subset
+ support_truncLT
+ support_truncLT_subset

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.

---

No changes to technical debt.

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

[wwylele]

How standard is the name "cardinality"? At first I thought this would be about the cardinality of the entire HahnSeries type (= card R ^ card Γ?). I convinced myself that this is the correct name by analogy to Multiset.card (viewing Multiset as Finsupp), but I'd like to know if this term already appears in the literature.

Other than this, looks good to me

[wwylele]

As the previous name was not wrong, I don't know if it is worth the churn to rename and deprecate

[vihdzp]

The idea here was to make the names of all these lemmas consistent. support_add_subset, support_sub_subset, support_smul_subset, etc. But I can revert if you want.

[vihdzp]

I can't really find anyone calling this anything beyond "the cardinality of the support". But I hope you agree that a more explicit name like cardinalMk_support would be overly verbose.

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[erdOne]

Thanks! This seems reasonable.
About the name: perhaps cardSupp? I don't have a strong opinion here.
maintainer delegate

[github-actions]

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

[jcommelin]

I second the cardSupp suggestion.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step