Commit 2024-02-21 14:19 24c9aaa1

View on Github →

feat: add kernel.(co)map_id (#10801)

Estimated changes

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.kernel.comapRight_id

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.comap_id'

added theorem ProbabilityTheory.kernel.comap_id

added theorem ProbabilityTheory.kernel.map_id'

added theorem ProbabilityTheory.kernel.map_id