Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-21 14:13 5cc2dfdd

View on Github →

feat(*): add various results split out from proof of Gallagher's theorem (#17985) This is a collection of tiny results that are not really related but I'm bundling them together in an effort to aid review.

Estimated changes

added theorem int.norm_coe_nat
deleted theorem nnnorm_nsmul_le
deleted theorem nnnorm_zsmul_le
deleted theorem norm_nsmul_le
added theorem norm_zpow_le_mul_norm
deleted theorem norm_zsmul_le