Commit 2022-01-18 10:53 a0da4f1f

View on Github →

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 σ.

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem equiv.perm.prod_comp'

added theorem equiv.perm.prod_comp

Modified src/data/finset/basic.lean

added theorem finset.map_perm

Modified src/data/finset/card.lean

added theorem finset.map_eq_of_subset

Modified src/linear_algebra/matrix/determinant.lean

Modified src/number_theory/sum_four_squares.lean