mathlib

4ca0a8b3 - feat(data/fintype/basic): provide a `fintype` instance for `sym α n` (#8427)

feat(data/fintype/basic): provide a `fintype` instance for `sym α n` (#8427) This also provides `fintype (sym.sym' α n)` as an intermediate step. Note we make `vector.perm.is_setoid` reducible as `quotient.fintype _` requires either this or `local attribute [instance] vector.perm.is_setoid` to be accepted by the elaborator. The referenced library note suggests making it reducible is fine. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>