Commit 2023-01-29 16:57 59ded3f3

View on Github →

feat port : Algebra.Free (#1353)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Free.lean

added inductive AddMagma.AssocRel

added def FreeAddMagma.length

added def FreeAddMagma.liftAux

added inductive FreeAddMagma

added structure FreeAddSemigroup

added theorem FreeMagma.hom_ext

added def FreeMagma.length

added theorem FreeMagma.length_toFreeSemigroup

added def FreeMagma.lift

added def FreeMagma.liftAux

added theorem FreeMagma.lift_comp_of'

added theorem FreeMagma.lift_comp_of

added theorem FreeMagma.lift_of

added def FreeMagma.map

added theorem FreeMagma.map_mul'

added theorem FreeMagma.map_of

added theorem FreeMagma.map_pure

added theorem FreeMagma.mul_bind

added theorem FreeMagma.mul_eq

added theorem FreeMagma.mul_map_seq

added theorem FreeMagma.mul_seq

added theorem FreeMagma.pure_bind

added theorem FreeMagma.pure_seq

added def FreeMagma.toFreeSemigroup

added theorem FreeMagma.toFreeSemigroup_comp_map

added theorem FreeMagma.toFreeSemigroup_comp_of

added theorem FreeMagma.toFreeSemigroup_map

added theorem FreeMagma.toFreeSemigroup_of

added theorem FreeMagma.traverse_eq

added theorem FreeMagma.traverse_mul'

added theorem FreeMagma.traverse_mul

added theorem FreeMagma.traverse_pure'

added theorem FreeMagma.traverse_pure

added inductive FreeMagma

added def FreeMagmaAssocQuotientEquiv

added theorem FreeSemigroup.head_mul

added theorem FreeSemigroup.hom_ext

added def FreeSemigroup.length

added theorem FreeSemigroup.length_map

added theorem FreeSemigroup.length_mul

added theorem FreeSemigroup.length_of

added def FreeSemigroup.lift

added theorem FreeSemigroup.lift_comp_of'

added theorem FreeSemigroup.lift_comp_of

added theorem FreeSemigroup.lift_of

added theorem FreeSemigroup.lift_of_mul

added def FreeSemigroup.map

added theorem FreeSemigroup.map_mul'

added theorem FreeSemigroup.map_of

added theorem FreeSemigroup.map_pure

added theorem FreeSemigroup.mk_mul_mk

added theorem FreeSemigroup.mul_bind

added theorem FreeSemigroup.mul_map_seq

added theorem FreeSemigroup.mul_seq

added def FreeSemigroup.of

added theorem FreeSemigroup.pure_bind

added theorem FreeSemigroup.pure_seq

added theorem FreeSemigroup.tail_mul

added theorem FreeSemigroup.traverse_eq

added theorem FreeSemigroup.traverse_mul'

added theorem FreeSemigroup.traverse_mul

added theorem FreeSemigroup.traverse_pure'

added theorem FreeSemigroup.traverse_pure

added structure FreeSemigroup

added theorem Magma.AssocQuotient.hom_ext

added def Magma.AssocQuotient.lift

added theorem Magma.AssocQuotient.lift_comp_of'

added theorem Magma.AssocQuotient.lift_comp_of

added theorem Magma.AssocQuotient.lift_of

added def Magma.AssocQuotient.map

added theorem Magma.AssocQuotient.map_of

added def Magma.AssocQuotient.of

added theorem Magma.AssocQuotient.quot_mk_assoc

added theorem Magma.AssocQuotient.quot_mk_assoc_left

added def Magma.AssocQuotient

added inductive Magma.AssocRel