Commit 2026-06-02 16:32 90aa2f5e

chore(Algebra/Polynomial/Module): workaround for backward.inferInstanceAs (#39011) This PR, like #38990, works around a backward.inferInstanceAs compatibility flag introduced by identifying PolynomialModule with Finsupp in our definitions. We introduce a new dsimp lemma funLike_eq that transfers the FunLike instances, and now we can use PolynomialModule's FunLike instance, instead of the custom CoeFun instance. This is not a great approach, but it seems the least painful for the short term. The alternative would be to strictly enforce the defeq barrier between PolynomialModule and Finsupp, which would mean a substantial rewrite of this corner of Mathlib. We can't make PolynomialModule an @[implicit_reducible], because we need different multiplication on it than Finsupp has.