mathlib
6a5764b3
- chore(analysis/normed_space/multilinear): use notation (#13452)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(analysis/normed_space/multilinear): use notation (#13452) * use notation `A [×n]→L[𝕜] B`; * use `A → B` instead of `Π x : A, B`.
Author
urkud
Parents
d81cedb1
Loading