This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
convert is_monoid_hom etc to structures, and move out of deprecated
#13506
Comments
4 tasks
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
The
deprecated/folder is no longer imported by mathlib. However there is something worth salvaging: theis_monoid_homclass, and all its relatives, could be converted to structures and moved back into mathlib.The text was updated successfully, but these errors were encountered: