mathlib3

3ff92489 - feat({group,ring}_theory/free_*): make free_ring.lift and free_comm_ring.lift equivs (#6364)

feat({group,ring}_theory/free_*): make free_ring.lift and free_comm_ring.lift equivs (#6364) This also adds `free_ring.hom_ext` and `free_comm_ring.hom_ext`, and deduplicates the definitions of the two lifts by introducing `abelian_group.lift_monoid`.