Commit 2024-04-03 17:37 6a3812f5

refactor(Algebra/Module): Use coercion from SemilinearMapClass to SemilinearMap (#10758) This PR adds a coercion from any instance of SemilinearMapClass to SemilinearMap. This is the standard practice for other parts of the library, such as ring homs (see also the recent change #10368). I also expect this change will help with some rough edges in #6057. Previously, a coercion from f : AlgHom to LinearMap would look like f.toNonUnitalAlgHom.toDistribMulActionHom.toLinearMap, now it should look like SemilinearMapClass.semilinearMap f. The new coercion instances are CoeHead since the left hand side is a free variable F. I redefined the existing DistribMulActionHom → LinearMap coercion in terms of the SemilinearMapClass coercion to ensure we don't get any diamonds.