Commit 2024-10-01 17:04 1fe4aec4

View on Github →

feat: ℂ and Finset.expect (#17274) Make more arguments to NNReal.coe_sum explicit to match NNReal.coe_expect. From LeanAPAP

Estimated changes

added theorem Finset.abs_expect_le
modified theorem RCLike.nnnorm_nnqsmul
added theorem RCLike.norm_expect_le
modified theorem RCLike.norm_nnqsmul
added theorem RCLike.ofReal_expect
added theorem Complex.im_nnqsmul
added theorem Complex.im_nsmul
added theorem Complex.im_qsmul
added theorem Complex.im_zsmul
added theorem Complex.re_nnqsmul
added theorem Complex.re_nsmul
added theorem Complex.re_qsmul
added theorem Complex.re_zsmul
added theorem Complex.im_expect
added theorem Complex.ofReal_expect
added theorem Complex.re_expect
added theorem NNReal.coe_expect
modified theorem NNReal.coe_prod
modified theorem NNReal.coe_sum
modified theorem Real.toNNReal_sum_of_nonneg