mathlib3

d550c3d0 - chore(*): Use `multilinear_map.mk_pi_algebra_fin` in place of a manual definition, and fix resulting errors

chore(*): Use `multilinear_map.mk_pi_algebra_fin` in place of a manual definition, and fix resulting errors This has the advantage of not needing the quotient. This also fixes some leftover `subtype.val` uses