mathlib

bc35902c - chore(algebra/group/hom): more generic `f x ≠ 1` lemmas (#12404)

chore(algebra/group/hom): more generic `f x ≠ 1` lemmas (#12404) * `map_ne_{one,zero}_iff` is the `not_congr` version of `map_eq_one_iff`, which was previously only available for `mul_equiv_class` * `ne_{one,zero}_of_map` is one direction of `map_ne_{one,zero}_iff` that doesn't assume injectivity Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>