Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-07 21:29 73f51b8e

View on Github →

feat(ring_theory/determinant): determinants (#404)

clean up determinant PR
remove unnecessary type annotations
update copyright
add additive version of prod_attach_univ

Estimated changes

Modified data/equiv/basic.lean

added theorem equiv.swap_apply_self

added theorem equiv.swap_mul_self

Modified data/fintype.lean

added theorem finset.prod_attach_univ

Modified group_theory/perm.lean

added theorem finset.prod_univ_perm

Created ring_theory/determinant.lean

added theorem matrix.det_diagonal

added theorem matrix.det_mul

added theorem matrix.det_mul_aux

added theorem matrix.det_one

added theorem matrix.det_zero