mathlib

2be2f2cb - feat(analysis/normed_space/multilinear): constant scalar multiplication is continuous (#15897)

feat(analysis/normed_space/multilinear): constant scalar multiplication is continuous (#15897) This PR adds an instance for continuous multilinear maps that gives continuous scalar multiplication.