Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 19:49 18f06ecf

View on Github →

chore(measure_theory/integral/interval_integral): generalize integral_smul (#9355) Make sure that it works for scalar multiplication by a complex number.

Estimated changes