Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-29 09:38 be61b02b

View on Github →

chore(analysis/normed/group/basic): Earlier ℝ lemmas (#16972) Move lemmas about the norm on ℝ from analysis.normed.field.basic to analysis.normed.group.basic. This avoids having to import normed_field to use real.norm_of_nonneg.

Estimated changes

deleted theorem real.ennnorm_eq_of_real
deleted theorem real.le_norm_self
deleted theorem real.nnnorm_coe_nat
deleted theorem real.nnnorm_of_nonneg
deleted theorem real.nnnorm_two
deleted theorem real.norm_coe_nat
deleted theorem real.norm_of_nonneg
deleted theorem real.norm_of_nonpos
deleted theorem real.norm_two
deleted theorem real.of_real_le_ennnorm
modified theorem real.to_nnreal_mul_nnnorm
added theorem real.le_norm_self
added theorem real.nnnorm_coe_nat
added theorem real.nnnorm_of_nonneg
added theorem real.nnnorm_two
added theorem real.norm_coe_nat
modified theorem real.norm_eq_abs
added theorem real.norm_of_nonneg
added theorem real.norm_of_nonpos
added theorem real.norm_two