Theorem Finset.prod_neg_index

Modification history

2025-03-20 22:56
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
chore(Algebra/Group): split off big operators from `Pointwise/Finset/Basic.lean` (#23156) …
Modified Finset.prod_neg_indexView on Github →
2023-12-27 20:59
Mathlib/Data/Finset/Pointwise.lean
feat: `(a • s)⁻¹ = s⁻¹ • a⁻¹` (#9199) …
Added Finset.prod_neg_indexView on Github →