Theorem MeasureTheory.toReal_rnDeriv_map

Modification history

2026-03-06 15:35
Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean
feat: Radon-Nikodym derivative of a map is a conditional expectation (#35089) …
Added MeasureTheory.toReal_rnDeriv_mapView on Github →