mathlib

71e11de8 - chore(analysis/normed/field/basic): add `@[simp]` to `real.norm_eq_abs (#15006)

chore(analysis/normed/field/basic): add `@[simp]` to `real.norm_eq_abs (#15006) * mark `real.norm_eq_abs` and `abs_nonneg` as `simp` lemmas; * add `abs` versions of `is_o.norm_left` etc; * add `inner_product_geometry.angle_smul_smul` and `linear_isometry.angle_map`.