Theorem Finset.prod_neg_index

Modification history

2026-09-18 15:04
Mathlib/Algebra/Group/Pointwise/Finset/BigOperators.lean
chore: catch up on a lot of `to_additive` debt (#43814) …
Modified Finset.prod_neg_indexView on Github →
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 →