Mathlib v3 is deprecated. Go to Mathlib v4

Theorem abs_norm_eq_norm

Modification history

2023-05-03 06:27
src/analysis/normed_space/basic.lean
chore(analysis/normed_space/basic): rename `abs_norm_eq_norm` to `abs_norm` (#18921)
Deleted abs_norm_eq_normView on Github →
2022-11-17 13:13
src/analysis/normed_space/basic.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified abs_norm_eq_normView on Github →
2021-10-01 13:24
src/analysis/normed_space/basic.lean
refactor(*): replace `abs` with vertical bar notation (#8891) …
Modified abs_norm_eq_normView on Github →
2020-10-01 07:41
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/inner_product): Define the inner product based on `is_R_or_C` (#4057)
Added abs_norm_eq_normView on Github →