# Commit 2021-02-16 12:05 2da1ab41

View on Github →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
```