∀ {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕜 F'] [inst_3 : NormedSpace ℝ F'] [inst_4 : CompleteSpace F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_5 : MeasureTheory.SigmaFinite (μ.trim hm)] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp F' 1 μ)),
  (MeasureTheory.condExpL1CLM F' hm μ) (c • f) = c • (MeasureTheory.condExpL1CLM F' hm μ) f