Theorem Finset.expect_boole_mul'

Modification history

2026-06-14 07:12

Mathlib/Algebra/BigOperators/Expect.lean

feat(Algebra/BigOperators/Expect): expectation of an indicator (#40388) …

Modified Finset.expect_boole_mul'View on Github →

2024-09-17 18:34

Mathlib/Algebra/BigOperators/Expect.lean

feat: Expectation of a function over a finset (#15883) …

Added Finset.expect_boole_mul'View on Github →