basic): Reindexing a product with a permutation (#11344)

Commit

3 years ago

feat(algebra/big_operators/basic): Reindexing a product with a permutation (#11344) This proves `(∏ x in s, f (σ x)) = ∏ x in s, f x` for a permutation `σ`.

Author

YaelDillies

Parents

8d5caba3

mathlib3 a0da4f1f - feat(algebra/big_operators/basic): Reindexing a product with a permutation (#11344)

mathlib3
a0da4f1f - feat(algebra/big_operators/basic): Reindexing a product with a permutation (#11344)