Theorem ProbabilityTheory.Kernel.coe_comap

Modification history

2025-03-01 01:15
Mathlib/Probability/Kernel/Composition/Basic.lean
chore: split Probability/Kernel/Composition/Basic (#22400) …
Modified ProbabilityTheory.Kernel.coe_comapView on Github →
2024-10-16 14:07
Mathlib/Probability/Kernel/Composition.lean
feat(Kernel): `κ.comap g = κ ∘ g` (#17823) …
Added ProbabilityTheory.Kernel.coe_comapView on Github →