Commit 2020-05-01 21:31 eb383b14

View on Github →

chore(group_theory/perm): delete duplicate lemmas (#2584) sum_univ_perm is a special case of sum_equiv, so it's not necessary. I also moved sum_equiv into the finset namespace.

Estimated changes

Modified src/data/fintype/card.lean

added theorem finset.prod_equiv

deleted theorem prod_equiv

Modified src/group_theory/perm/sign.lean

deleted theorem finset.prod_univ_perm

deleted theorem finset.sum_univ_perm

Modified src/linear_algebra/determinant.lean

Modified src/number_theory/sum_four_squares.lean