Theorem ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id

Modification history

2026-05-08 06:03
Mathlib/Probability/Kernel/Composition/KernelLemmas.lean
chore(Mathlib/Probability/Kernel/Composition/KernelLemmas.lean): automated extraction (#39042) …
Modified ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_idView on Github →
2026-03-27 14:36
Mathlib/Probability/Kernel/Composition/KernelLemmas.lean
feat(Kernel/Category): Stoch is a Markov category (#36779) …
Added ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_idView on Github →