Def MeasureTheory.condExpUnexpander

Modification history

2025-11-19 06:07
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
chore: move Mathlib to the module system (#31786) …
Deleted MeasureTheory.condExpUnexpanderView on Github →
2025-03-09 07:00
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
fix: prevent probability notation clashing with list notation (#22699) …
Added MeasureTheory.condExpUnexpanderView on Github →