Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 17:41 70759ef9

View on Github →

feat(analysis): lemmas about nnnorm and nndist (#13498) Most of these lemmas follow trivially from the norm versions. This is far from exhaustive. Additionally:

  • nnreal.coe_supr and nnreal.coe_infi are added
  • The old is_primitive_root.nnnorm_eq_one is renamed to is_primitive_root.norm'_eq_one as it was not about nnnorm at all. The unprimed name is already taken in reference to algebra.norm.
  • parallelogram_law_with_norm_real is removed since it's syntactically identical to parallelogram_law_with_norm ℝ and also not used anywhere.

Estimated changes

added theorem complex.conj_cle_nnorm
added theorem complex.im_clm_nnnorm
added theorem complex.re_clm_nnnorm
added theorem nnnorm_inner_le_nnnorm
modified theorem parallelogram_law_with_norm
added theorem matrix.nnnorm_le_iff
added theorem matrix.nnnorm_lt_iff
added theorem coe_comp_nnnorm
added theorem nnnorm_le_insert'
added theorem nnnorm_le_insert
added theorem nnnorm_le_pi_nnnorm
added theorem pi_nnnorm_le_iff
added theorem pi_nnnorm_lt_iff
added theorem finset.nnnorm_prod_le'
added theorem finset.nnnorm_prod_le
added theorem list.nnnorm_prod_le'
added theorem list.nnnorm_prod_le
added theorem units.nnorm_pos
added theorem pi_Lp.nnnorm_eq
added theorem nnnorm_star
added theorem quaternion.nnorm_coe
modified theorem nnreal.coe_Inf
modified theorem nnreal.coe_Sup
added theorem nnreal.coe_image
added theorem nnreal.coe_infi
added theorem nnreal.coe_supr
added theorem isometry.nndist_eq