Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Add an instance {add_,}sub{monoid,group}_class S M → has_coe_t S ({add_,}sub{monoid,group} M) #15053

Open
Vierkantor opened this issue Jun 29, 2022 · 0 comments

Comments

@Vierkantor
Copy link
Collaborator

We are missing instances add_submonoid_class S M → has_coe S (add_submonoid M) (probably has_coe_t now that I think of it), so we can just use coe here.

Similar coercions should also be added for subgroup and other subobjects.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant