Commit 2021-03-15 17:06 d9dc30e5

View on Github →

feat(algebra/free): turn free_magma.lift into an equivalence (#6672) This will be convenient for some work I have in mind and is more consistent with the pattern used elsewhere, such as:

free_algebra.lift
monoid_algebra.lift
universal_enveloping.lift
...

Estimated changes

Modified src/algebra/free.lean

deleted def free_add_magma.lift

added def free_add_magma.lift_aux

modified def free_magma.lift

added def free_magma.lift_aux

added theorem free_magma.lift_aux_unique

deleted theorem free_magma.lift_mul

deleted theorem free_magma.lift_unique