basic): make `inclusion` a `ring_hom`, not a `monoid_hom` (#13746)

Commit

3 years ago

fix(ring_theory/subsemiring/basic): make `inclusion` a `ring_hom`, not a `monoid_hom` (#13746)

Author

j-loreaux

Parents