Theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'

Modification history

2025-01-04 12:41

Mathlib/Probability/Kernel/MeasurableIntegral.lean

chore: split Kernel/MeasurableIntegral (#20427) …

Modified ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'View on Github →

2024-07-23 07:55

Mathlib/Probability/Kernel/MeasurableIntegral.lean

refactor(Probability): Make kernels a type (#15021) …

Added ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'View on Github →

2023-06-16 12:59

Mathlib/Probability/Kernel/MeasurableIntegral.lean

feat: port Probability.Kernel.Composition (#5044)

Deleted ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'View on Github →

2023-06-14 01:02

Mathlib/Probability/Kernel/MeasurableIntegral.lean

feat: port Probability.Kernel.MeasurableIntegral (#4884)

Added ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'View on Github →