Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-13 09:58 88fb7cab

View on Github →

chore(analysis/calculus): move the definition of formal_multilinear_series to a new file (#5348)

Estimated changes

Created src/analysis/calculus/formal_multilinear_series.lean

added theorem formal_multilinear_series.congr

added def formal_multilinear_series.shift

added def formal_multilinear_series.unshift

added def formal_multilinear_series

Modified src/analysis/calculus/times_cont_diff.lean

deleted theorem formal_multilinear_series.congr

deleted def formal_multilinear_series.restrict_scalars

deleted def formal_multilinear_series.shift

deleted def formal_multilinear_series.unshift

deleted def formal_multilinear_series