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.