Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-03 06:27 f9dd3204

View on Github →

chore(analysis/normed_space/basic): rename abs_norm_eq_norm to abs_norm (#18921)

Estimated changes

added theorem abs_norm
deleted theorem abs_norm_eq_norm