Commit 2023-07-01 10:20 6f81a92b

View on Github →

feat: algebraMap_mem for SetLike instances (#5594) This adds an algebraMap_mem in the root namespace and protects Subalgebra.algebraMap_mem. The new declaration holds for terms of S where S is a Setlike satisfying OneMemClass S A and SMulMemClass S R A and A is an R-algebra.

Estimated changes