mathlib3
88fb7cab - chore(analysis/calculus): move the definition of `formal_multilinear_series` to a new file (#5348)

Commit

5 years ago

chore(analysis/calculus): move the definition of `formal_multilinear_series` to a new file (#5348) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

urkud

Parents

36eec1a9

mathlib3 88fb7cab - chore(analysis/calculus): move the definition of `formal_multilinear_series` to a new file (#5348)

mathlib3
88fb7cab - chore(analysis/calculus): move the definition of `formal_multilinear_series` to a new file (#5348)