Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-02 14:25 bfbd0937

View on Github →

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.

Estimated changes

deleted theorem inv.is_group_hom
deleted theorem is_add_group_hom.map_sub
deleted theorem is_add_group_hom.sub
deleted theorem is_group_hom.inv
deleted theorem is_group_hom.map_inv
deleted theorem is_group_hom.map_one
deleted theorem is_group_hom.mk'
deleted theorem is_group_hom.mul
deleted theorem is_monoid_hom.map_mul
deleted theorem is_monoid_hom.of_mul
deleted theorem is_mul_hom.inv
deleted theorem is_mul_hom.mul
deleted theorem monoid_hom.coe_of
deleted def monoid_hom.of
deleted theorem is_unit.map'
deleted theorem units.coe_map'
deleted def units.map'
modified def with_one.lift
modified theorem with_one.lift_coe
modified theorem with_one.lift_one
modified theorem with_one.lift_unique
modified def with_one.map
deleted theorem with_one.map_eq
added theorem inv.is_group_hom
added theorem is_add_group_hom.sub
added theorem is_group_hom.inv
added theorem is_group_hom.map_inv
added theorem is_group_hom.map_one
added theorem is_group_hom.mk'
added theorem is_group_hom.mul
added theorem is_monoid_hom.map_mul
added theorem is_monoid_hom.of_mul
added theorem is_mul_hom.inv
added theorem is_mul_hom.mul
added theorem is_unit.map'
added theorem monoid_hom.coe_of
added def monoid_hom.of
added theorem units.coe_map'
added def units.map'