Commit 2023-05-24 10:36 a40639ab

View on Github →

feat: port Analysis.Normed.MulAction + #19053 (#4288) Both the new file and the other fixes are done in the same PR, since according to the description of leanprover-community/mathlib#19053 "this should be very easy to forward-port".

Estimated changes

added theorem dist_smul_le
added theorem dist_smul₀
added theorem lipschitzWith_smul
added theorem nndist_smul_le
added theorem nndist_smul₀
added theorem nnnorm_smul
added theorem nnnorm_smul_le
added theorem norm_smul
added theorem norm_smul_le
deleted theorem dist_smul_le
deleted theorem dist_smul₀
deleted theorem lipschitzWith_smul
deleted theorem nndist_smul_le
deleted theorem nndist_smul₀
deleted theorem nnnorm_smul
deleted theorem nnnorm_smul_le
deleted theorem norm_smul
deleted theorem norm_smul_le