Theorem ProbabilityTheory.Kernel.lintegral_id'

Modification history

2025-02-27 10:04

Mathlib/Probability/Kernel/Basic.lean

feat: add lemmas about kernels (#22200)

Added ProbabilityTheory.Kernel.lintegral_id'View on Github →