Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-15 03:41 6a5764b3

View on Github →

chore(analysis/normed_space/multilinear): use notation (#13452)

  • use notation A [×n]→L[𝕜] B;
  • use A → B instead of Π x : A, B.

Estimated changes