mathlib3
07ae80f4 - refactor(algebra/*): delete `free_monoid` from `algebra/free`, restore some functions in `algebra/group/with_one` (#1227)

Commit
6 years ago
refactor(algebra/*): delete `free_monoid` from `algebra/free`, restore some functions in `algebra/group/with_one` (#1227) * refactor(algebra/*): Remove `free_monoid` from `algebra/free`, fixes #929 * use `namespace with_one` * Add `with_one.coe_is_mul_hom` * Restore `with_one.lift` etc from `algebra/free` `free_monoid.lift` etc * Define `with_one.map` based on the deleted `free_monoid.map` Define using `option.map`, and prove equivalence to `λ f, lift $ coe ∘ f`.
Author
Committer
Parents
Loading