Theorem ContinuousLinearMap.integral_comp_commSL

Modification history

2025-09-23 13:41

Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

chore(MeasureTheory): semilinearize composition of integrals with CLM (#29853)

Added ContinuousLinearMap.integral_comp_commSL View on Github →