Commit 2021-02-16 12:05 2da1ab41

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:

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