Def ProbabilityTheory.Kernel.discard

Modification history

2026-03-16 15:03
Mathlib/Probability/Kernel/Basic.lean
refactor(Kernel.discard): redefine using `PUnit` (#36687) …
Modified ProbabilityTheory.Kernel.discardView on Github →
2024-11-28 16:12
Mathlib/Probability/Kernel/Basic.lean
feat(Probability): identity, copy, discard and swap kernels (#19481) …
Added ProbabilityTheory.Kernel.discardView on Github →