Theorem MeasureTheory.lpMeasSubgroup_coe

Modification history

2025-02-25 15:16
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
chore(MeasureTheory/Function/ConditionalExpectation): remove unneeded `lpMeasSubgroup_coe` and `lpMeas_coe` (#22214) …
Deleted MeasureTheory.lpMeasSubgroup_coeView on Github →
2023-06-13 09:59
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
feat: port MeasureTheory.Function.ConditionalExpectation.AEMeasurable (#5005)
Added MeasureTheory.lpMeasSubgroup_coeView on Github →