mathlib

d61d8bfe - feat(measure_theory/bochner_integration): extend the integral_smul lemmas (#6654)

feat(measure_theory/bochner_integration): extend the integral_smul lemmas (#6654) Extend the `integral_smul` lemmas to multiplication of a function `f : α → E` with scalars in `𝕜` with `[nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class ℝ 𝕜 E]` instead of only `ℝ`.