feat: define map from PowerSeries to FormalMultilinearSeries

[Paul-Lez]

WIP.

This PR defines a map from PowerSeries R to FormalMultilinearSeries R A A, and proves that this map preserves addition and composition.

Xavier Genereux xaviergenereux@hotmail.com

---

[github-actions]

PR summary 2c60d0e46e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.PowerSeries.ToFormalMultilinearSeries (new file)	1919

---

Declarations diff

+ Composition.asFinsuppAntidiag
+ Composition.ofFinsuppAntidiag
+ Finset.sigma_filter
+ FormalMultilinearSeries.applyComposition_apply_prod
+ List.filter_nezero_sum
+ List.prod_ofFn_smul
+ PowerSeries.toFormalMultilinearSeries
+ apply_pos_of_prod_ne_zero
+ coeff_subst_comp
+ mkPiAlgebraFin_ne_zero
+ ofFn_prod_one
+ posAntidiagonals
+ prod_univ_embedding
+ sum_sigma_range_eq_sum_posAntidiagonals
+ toFormalMultilinearSeries_comp
+ toFormalMultilinearSeries_inj

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.