mathlib3

3d1f16aa - feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316)

feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316) I'm going to use this definition for converting `(mv_)power_series` to `formal_multilinear_series`.