feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas

[vasnesterov]

Define Multiseries and MultiseriesExpansion and restate some Seq API for Multiseries.

---

This is a part of the compute_asymptotics tactic (#28291).

[github-actions]

PR summary ea886ccefe

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic	1
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (new file)	604

---

Declarations diff

+ Basis
+ Multiseries
+ MultiseriesExpansion
+ Pairwise_cons_nil
+ Pairwise_nil
+ cons
+ cons_eq_cons
+ cons_ne_nil
+ const_toFun
+ corec
+ corec_cons
+ corec_nil
+ destruct
+ destruct_cons
+ destruct_eq_cons
+ destruct_eq_destruct_map
+ destruct_eq_none
+ destruct_nil
+ eq_mk
+ eq_of_bisim
+ eq_of_bisim_strong
+ head
+ head_cons
+ head_nil
+ instance (basis : Basis) : Inhabited (MultiseriesExpansion basis)
+ instance (basis_hd basis_tl) : Inhabited (Multiseries basis_hd basis_tl)
+ instance {basis_hd basis_tl} :
+ map
+ map_comp
+ map_cons
+ map_id
+ map_nil
+ mem_cons_iff
+ mk
+ mk_eq_mk_iff
+ mk_eq_mk_iff_iff
+ mk_replaceFun
+ mk_seq
+ mk_toFun
+ ms_eq_mk_iff
+ ms_eq_ms_iff_mk_eq_mk
+ nil
+ nil_ne_cons
+ notMem_nil
+ ofReal
+ replaceFun
+ replaceFun_seq
+ replaceFun_toFun
+ seq
+ tail
+ tail_cons
+ tail_nil
+ toFun
+ toReal
+ toSeq
++ recOn

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

[mathlib-merge-conflicts]

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