Theorem MeasureTheory.condExp_ofNat

Modification history

2025-01-26 17:26
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat: `μ[ofNat n * f|m] =ᵐ[μ] ofNat n * μ[f|m]` (#21001) …
Added MeasureTheory.condExp_ofNatView on Github →