Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 21:09 08ea23b2

View on Github →

refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs (#6311) This removes:

  • free_group.to_group.to_fun and free_group.to_group, as these are both subsumed by the stronger lift.
  • abelianization.hom_equiv as this is now abelianization.lift.symm
  • free_abelian_group.hom_equiv as this is now free_abelian_group.lift.symm

Estimated changes

modified def abelianization.lift
added theorem free_group.lift.mk
added theorem free_group.lift.of
added theorem free_group.lift.of_eq
added theorem free_group.lift.unique
modified def free_group.lift
added theorem free_group.map_eq_lift
modified def free_group.prod
deleted theorem free_group.to_group.mk
deleted theorem free_group.to_group.of
deleted theorem free_group.to_group.of_eq
deleted def free_group.to_group
modified theorem presented_group.to_group.of