Commit 2025-12-18 07:31 422a9f16

chore(Algebra/Module): make select Module assumptions (#32435) This solves a thorny issue that we have when working with homological algebra: an element X : ModuleCat ℤ by construction contain the data of two (propeq) Module ℤ X instances. Instead of fighting typeclasses at the point of use, it is enough to make the Module ℤ X assumptions that can be inferred from other arguments actually be inferred by unification, rather than filled in with typeclass search. This PR does precisely that for the handful of definitions that are particularly problematic for the purpose of CFT. This is not unlike the status of MeasurableSpace in the measure theory library, and in fact there already existed a library note explaining this design decision, but it didn't cover that use case, so I expanded it. From ClassFieldTheory