mathlib3
08ea23b2 - refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs (#6311)

Commit
4 years ago
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`
Author
Parents
Loading