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.