Commit 2020-12-03 16:31 52697178

View on Github →

chore(linear_algebra/determinant): Move some lemmas about swaps to better files (#5201) These lemmas are not specific to determinants, and I need them in another file imported by determinant.

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.apply_swap_eq_self

modified theorem equiv.comp_swap_eq_update

modified theorem equiv.swap_apply_self

Modified src/group_theory/perm/sign.lean

added def equiv.perm.mod_swap

Modified src/linear_algebra/determinant.lean

deleted def matrix.mod_swap