Theorem ProbabilityTheory.Kernel.discard_eq_const

Modification history

2026-03-16 15:03
Mathlib/Probability/Kernel/Basic.lean
refactor(Kernel.discard): redefine using `PUnit` (#36687) …
Modified ProbabilityTheory.Kernel.discard_eq_constView on Github →
2025-08-04 07:37
Mathlib/Probability/Kernel/Basic.lean
feat(Probability): lemmas about `Kernel.discard` (#27584)
Added ProbabilityTheory.Kernel.discard_eq_constView on Github →