mathlib3

ce11c3c2 - refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140)

refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140) There is no need to include this argument in the type of `multilinear_map`, as it is only used to state the propositions. Instead, we move it into a binder in the `map_add` and `map_smul` fields. The same trick is done for the relation for `pi_tensor_product`. The benefit here is pretty marginal; the main one is that `mutlilinear_map.mk_pi_algebra` no longer requires a `decidable_eq I` instance. However, it still requires `fintype I`, and in practice all computably finite types are also computably decidable. This does at least mean that `0 : multilinear_map ...` rightfully no longer requires decidable equality! The downside of this PR is that the `map_add'` and `map_smul'` fields are often more annoying to prove as there are sometimes duplicate decidable instances to eliminate. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/A.20possible.20diamond/near/260179946)