Commit 2021-04-10 06:53 7ae2af63

feat(group_theory/is_free_group): promote is_free_group.lift' to an equiv (#7110) While non-computable, this makes the API of is_free_group align more closely with free_group. Based on discussion in the original PR, this doesn't go as far as changing the definition of is_free_group to take the equiv directly. This additionally:

• adds the definition lift, a universe polymorphic version of lift'
• adds the lemmas:
  • lift'_eq_free_group_lift
  • lift_eq_free_group_lift
  • of_eq_free_group_of
  • ext_hom'
  • ext_hom
• renames is_free_group.iso_free_group_of_is_free_group to the shorter is_free_group.to_free_group
• removes lemmas absent from the free_group API that are no longer needed for the proofs here:
  • end_is_id
  • eq_lift