Theorem ContinuousLinearMap.smul_compLp
Modification history
2025-09-23 13:41
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
chore(MeasureTheory): semilinearize composition of integrals with CLM (#29853)
Modified ContinuousLinearMap.smul_compLpView on Github →