Revision #2178 → #2568 · back to history
255dae7266d6| Field | From #2178 | To #2568 |
|---|---|---|
| mathlib.decl | MeasureTheory.integral_pdf_smul | MeasureTheory.pdf.integral_pdf_smul |
| provenance | ai | ai-moderated |
19ac8192e395| Field | From #2178 | To #2568 |
|---|---|---|
| mathlib.decl | MeasureTheory.lintegral_eq_integral_meas_lt | MeasureTheory.Integrable.integral_eq_integral_meas_lt |
| provenance | ai | ai-moderated |