Theorem finprod_mem_powerset_insert

Modification history

2025-08-01 20:41

Mathlib/Algebra/BigOperators/Finprod.lean

feat(Algebra/BigOperators/Finprod): add powerset projection lemmas (#25965) …

Added finprod_mem_powerset_insert View on Github →