Theorem Finset.expect_indicator_one

Modification history

2026-06-14 07:12

Mathlib/Algebra/BigOperators/Expect.lean

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

Added Finset.expect_indicator_one View on Github →