Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 23:18 71e11de8

View on Github →

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.

Estimated changes

modified theorem abs_nonneg
modified def complex.im_clm
modified def complex.re_clm
modified theorem real.norm_eq_abs