mathlib
58de2a0a - chore(analysis): use nnnorm notation everywhere (#13930)

Commit

3 years ago

chore(analysis): use nnnorm notation everywhere (#13930) This was done with a series of ad-hoc regular expressions, then cleaned up by hand.

Author

eric-wieser

Parents