mathlib
mathlib copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
Add an instance `{add_,}sub{monoid,group}_class S M → has_coe_t S ({add_,}sub{monoid,group} M)`
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.
