mathlib

17ef379e - refactor(analysis): change the symbol for norm to align with the unicode spec (#17575)

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) The characters in question are: * U+2016 DOUBLE VERTICAL LINE `‖`. The Unicode Character Database says "used in pairs to indicate norm of a matrix", for instance [here](https://www.fileformat.info/info/unicode/char/2016/index.htm) and [here](https://unicode-explorer.com/c/2016) * U+2225 PARALLEL TO `∥`. On some platforms this renders with a forward slant! Previously `norm` was the latter and `parallel` was the former. This change swaps them around: * `∥x∥`, `S ‖ T`: before * `‖x‖`, `S ∥ T`: after Code using U+2016 `‖` for fintype cardinality has been left unchanged.