Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-03 11:06 44b58b42

View on Github →

feat(topology/algebra/module/multilinear): add continuous versions of constructions (#18044) One of these is a much more general case of continuous_multilinear_map.curry0; but to keep this PR small we don't attempt to remove curry0, instead just golfing it.

Estimated changes