mathlib3

2da1ab41 - feat(data/equiv): Add lemmas to reduce `@finset.univ (perm (fin n.succ)) _` (#5593)

feat(data/equiv): Add lemmas to reduce `@finset.univ (perm (fin n.succ)) _` (#5593) The culmination of these lemmas is that `matrix.det` can now be reduced by a minimally steered simp: ```lean import data.matrix.notation import group_theory.perm.fin import linear_algebra.determinant open finset example {α : Type} [comm_ring α] {a b c d : α} : matrix.det ![![a, b], ![c, d]] = a * d - b * c := begin simp [matrix.det, univ_perm_fin_succ, ←univ_product_univ, sum_product, fin.sum_univ_succ, fin.prod_univ_succ], ring end ``` Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>