Theorem prod_indicator

Modification history

2024-10-27 19:58

Mathlib/Algebra/BigOperators/Pi.lean

feat: a product of indicators is the indicator of the product (#17964)

Added prod_indicator View on Github →