Theorem Fintype.prod_sum_elim

Modification history

2025-02-20 18:07

Mathlib/Data/Fintype/BigOperators.lean

chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130)

Deleted Fintype.prod_sum_elim View on Github →

2023-01-21 14:22

Mathlib/Data/Fintype/BigOperators.lean

feat: port Data.Fintype.BigOperators (#1742)

Added Fintype.prod_sum_elim View on Github →