Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-19 07:18 3c422528

View on Github →

refactor(analysis/normed/group/hom): split (#18219) Half of this file is completely elementary, able to be proved directly from the definitions in normed/group/hom/basic after a few instances are added there. The other half consists of technical lemmas from LTE, never used elsewhere in mathlib, and requires more imports. Since this file is imported by many files (including data/complex/is_R_or_C, see #18217 for a discussion of what that file imports), I propose splitting off the LTE half.

Estimated changes

deleted theorem int.norm_cast_rat
deleted theorem int.norm_cast_real
deleted theorem int.norm_coe_nat
deleted theorem int.norm_eq_abs
deleted theorem nnnorm_zpow_le_mul_norm
deleted theorem nnreal.coe_nat_abs
deleted theorem norm_zpow_le_mul_norm
deleted theorem rat.norm_cast_real
added theorem int.norm_cast_rat
added theorem int.norm_cast_real
added theorem int.norm_coe_nat
added theorem int.norm_eq_abs
added theorem nnreal.coe_nat_abs
added theorem norm_zpow_le_mul_norm
added theorem rat.norm_cast_real