Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 20:30 090e59d0

View on Github →

feat(analysis/normed_space/operator_norm): norm of lsmul (#13538)

  • From the sphere eversion project
  • Required for convolutions

Estimated changes