Commit 2026-08-10 23:43 6f1ef4e5

feat: generalize transfer instance type class assumptions (#42291) This PR refactors various declarations that are used for transporting instances or definitions along equivalences. The idea is to avoid using local instances with letI in places where we can assume an arbitrary instance instead, because otherwise these declarations can only be used in situations where the global instance is defeq to the one introduced by letI. In many cases this means that the equivalence needs to be an AddEquiv or LinearEquiv instead of an Equiv. This is not an issue in practice, because it is typically easy to construct this richer equivalence. It would be possible to keep both styles of transporting declarations, but I think that would be more confusing. This PR is a prerequisite for #41362 (no_exposing some operations in MonoidAlgebra), because to use the old Equiv.distribMulAction we need the MonoidAlgebra instances to be exposed.