Commit 2026-10-29 18:27 f1a9649a
View on Github →chore(MeasureTheory): generalize CircleIntegrable.const_smul (#45189)
This lemma unnecessarily assumed that the ring of scalars is the same as the codomain of the function. Two other lemmas are also generalized from NormSMulClass to IsBoundedSMul.