Commit 2023-03-30 18:52 ce11c3c2

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