Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-14 20:57
446123f7
View on Github →
chore(Probability/Kernel): turn
isSFiniteKernel_sum
into an instance (
#21862
)
Estimated changes
Modified
Mathlib/Probability/Kernel/Composition/Basic.lean
Modified
Mathlib/Probability/Kernel/Defs.lean
deleted
theorem
ProbabilityTheory.Kernel.isSFiniteKernel_sum
Modified
Mathlib/Probability/Kernel/WithDensity.lean