Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 c64b9224

View on Github →

refactor(algebra/free): review API, redefine free_semigroup (#17144)

Estimated changes

Modified src/algebra/free.lean

added inductive add_magma.assoc_rel

deleted inductive add_magma.free_add_semigroup.r

modified def free_add_magma.length

deleted def free_add_magma.map

deleted def free_add_semigroup.lift'

added structure free_add_semigroup

added theorem free_magma.hom_ext

modified def free_magma.length

added theorem free_magma.length_to_free_semigroup

deleted theorem free_magma.lift_aux_unique

added theorem free_magma.lift_comp_of'

added theorem free_magma.lift_comp_of

modified def free_magma.map

deleted theorem free_magma.map_mul

added def free_magma.to_free_semigroup

added theorem free_magma.to_free_semigroup_comp_map

added theorem free_magma.to_free_semigroup_comp_of

added theorem free_magma.to_free_semigroup_map

added theorem free_magma.to_free_semigroup_of

added def free_magma_assoc_quotient_equiv

added theorem free_semigroup.head_mul

added theorem free_semigroup.hom_ext

added def free_semigroup.length

added theorem free_semigroup.length_map

added theorem free_semigroup.length_mul

added theorem free_semigroup.length_of

deleted def free_semigroup.lift'

modified def free_semigroup.lift

added theorem free_semigroup.lift_comp_of'

added theorem free_semigroup.lift_comp_of

deleted theorem free_semigroup.lift_mul

modified theorem free_semigroup.lift_of_mul

deleted theorem free_semigroup.lift_unique

modified def free_semigroup.map

deleted theorem free_semigroup.map_mul

added theorem free_semigroup.mk_mul_mk

modified def free_semigroup.of

added theorem free_semigroup.tail_mul

added structure free_semigroup

deleted def free_semigroup

deleted def free_semigroup_free_magma

deleted theorem free_semigroup_free_magma_mul

added theorem magma.assoc_quotient.hom_ext

added def magma.assoc_quotient.lift

added theorem magma.assoc_quotient.lift_comp_of'

added theorem magma.assoc_quotient.lift_comp_of

added theorem magma.assoc_quotient.lift_of

added def magma.assoc_quotient.map

added theorem magma.assoc_quotient.map_of

added def magma.assoc_quotient.of

added theorem magma.assoc_quotient.quot_mk_assoc

added theorem magma.assoc_quotient.quot_mk_assoc_left

added def magma.assoc_quotient

added inductive magma.assoc_rel

deleted def magma.free_semigroup.lift

deleted theorem magma.free_semigroup.lift_mul

deleted theorem magma.free_semigroup.lift_of

deleted theorem magma.free_semigroup.lift_unique

deleted def magma.free_semigroup.map

deleted theorem magma.free_semigroup.map_mul

deleted theorem magma.free_semigroup.map_of

deleted def magma.free_semigroup.of

deleted theorem magma.free_semigroup.of_mul

deleted theorem magma.free_semigroup.of_mul_assoc

deleted theorem magma.free_semigroup.of_mul_assoc_left

deleted theorem magma.free_semigroup.of_mul_assoc_right

deleted inductive magma.free_semigroup.r

deleted def magma.free_semigroup

Modified src/algebra/hom/equiv.lean

added def mul_hom.to_mul_equiv