Commit 2026-03-16 15:03 fd5d8fca

View on Github →

refactor(Kernel.discard): redefine using PUnit (#36687) Make Kernel.discard universe-polymorphic. The main purpose is to use this kernel in categories.

Estimated changes

Modified Mathlib/Probability/Kernel/Basic.lean

modified def ProbabilityTheory.Kernel.discard

modified theorem ProbabilityTheory.Kernel.discard_apply

modified theorem ProbabilityTheory.Kernel.discard_eq_const

Modified Mathlib/Probability/Kernel/Composition/Comp.lean