mathlib3
ab64f631 - refactor(algebra/sub{monoid,group,ring,semiring,field}): merge together the `restrict` and `cod_restrict` helpers (#14548)

Commit
3 years ago
refactor(algebra/sub{monoid,group,ring,semiring,field}): merge together the `restrict` and `cod_restrict` helpers (#14548) This uses the new subobject typeclasses to merge together: * `monoid_hom.mrestrict`, `monoid_hom.restrict` * `monoid_hom.cod_mrestrict`, `monoid_hom.cod_restrict` * `ring_hom.srestrict`, `ring_hom.restrict`, `ring_hom.restrict_field` * `ring_hom.cod_srestrict`, `ring_hom.cod_restrict`, `ring_hom.cod_restrict_field` For consistency, this also removes the `m` prefix from `mul_hom.mrestrict`
Author
Parents
Loading