mathlib3

bfbd0937 - chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` (#2056)

chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` (#2056) * Move `is_mul/monoid/group_hom` to `deprecated/` Also improve deprecation docstring. TODO: fix compile * chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` Also migrate a few definitions to bundled homs: * use `monoid_hom.map_is_conj` instead of `is_group_hom.is_conj`; * `with_one.lift` and `with_one.map` now take `f` and an explicit argument `h : ∀ x y, f (x * y) = f x * f y` instead of `f` and `[is_mul_hom f]`, and produce a `monoid_hom`. As a side effect, they are now defined for semigroup homomorphisms only. * Adjust module docstring * Update src/algebra/group/with_one.lean I wonder if mergify will do its job now. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>