Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-19 14:39 07ae80f4

View on Github →

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.

Estimated changes

Modified src/algebra/free.lean

deleted def semigroup.free_monoid.lift

deleted theorem semigroup.free_monoid.lift_mul

deleted theorem semigroup.free_monoid.lift_of

deleted theorem semigroup.free_monoid.lift_one

deleted theorem semigroup.free_monoid.lift_unique

deleted def semigroup.free_monoid.map

deleted theorem semigroup.free_monoid.map_mul

deleted theorem semigroup.free_monoid.map_of

deleted def semigroup.free_monoid.of

deleted theorem semigroup.free_monoid.of_mul

deleted def semigroup.free_monoid

Modified src/algebra/group/with_one.lean

modified theorem with_one.coe_inj

modified theorem with_one.coe_ne_one

added def with_one.lift

added theorem with_one.lift_coe

added theorem with_one.lift_one

added theorem with_one.lift_unique

added def with_one.map

added theorem with_one.map_eq

modified theorem with_one.mul_coe

modified theorem with_one.ne_one_iff_exists

modified theorem with_one.one_ne_coe