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
added theorem mul_mem_ball_mul_iff
added theorem nnnorm_pow_le_mul_norm
added theorem norm_pow_le_mul_norm
added theorem pow_mem_ball
added theorem pow_mem_closed_ball
deleted theorem int.norm_coe_nat
added theorem set.image_Sup
modified theorem filter.mono_bliminf'
modified theorem filter.mono_bliminf
modified theorem filter.mono_blimsup'
modified theorem filter.mono_blimsup