Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-12 12:59 3fe449e1

View on Github →

feat(algebra/free): free magma, semigroup, monoid (#735)

Estimated changes

Created src/algebra/free.lean

added def free_magma.length

added def free_magma.lift

added theorem free_magma.lift_mul

added theorem free_magma.lift_of

added theorem free_magma.lift_unique

added def free_magma.map

added theorem free_magma.map_mul'

added theorem free_magma.map_mul

added theorem free_magma.map_of

added theorem free_magma.map_pure

added theorem free_magma.mul_bind

added theorem free_magma.mul_map_seq

added theorem free_magma.mul_seq

added theorem free_magma.pure_bind

added theorem free_magma.pure_seq

added def free_magma.repr'

added theorem free_magma.traverse_eq

added theorem free_magma.traverse_mul'

added theorem free_magma.traverse_mul

added theorem free_magma.traverse_pure'

added theorem free_magma.traverse_pure

added inductive free_magma

added def free_semigroup.lift'

added def free_semigroup.lift

added theorem free_semigroup.lift_mul

added theorem free_semigroup.lift_of

added theorem free_semigroup.lift_of_mul

added theorem free_semigroup.lift_unique

added def free_semigroup.map

added theorem free_semigroup.map_mul'

added theorem free_semigroup.map_mul

added theorem free_semigroup.map_of

added theorem free_semigroup.map_pure

added theorem free_semigroup.mul_bind

added theorem free_semigroup.mul_map_seq

added theorem free_semigroup.mul_seq

added def free_semigroup.of

added theorem free_semigroup.pure_bind

added theorem free_semigroup.pure_seq

added def free_semigroup.traverse'

added theorem free_semigroup.traverse_eq

added theorem free_semigroup.traverse_mul'

added theorem free_semigroup.traverse_mul

added theorem free_semigroup.traverse_pure'

added theorem free_semigroup.traverse_pure

added def free_semigroup

added def free_semigroup_free_magma

added theorem free_semigroup_free_magma_mul

added def magma.free_semigroup.lift

added theorem magma.free_semigroup.lift_mul

added theorem magma.free_semigroup.lift_of

added theorem magma.free_semigroup.lift_unique

added def magma.free_semigroup.map

added theorem magma.free_semigroup.map_mul

added theorem magma.free_semigroup.map_of

added def magma.free_semigroup.of

added theorem magma.free_semigroup.of_mul

added theorem magma.free_semigroup.of_mul_assoc

added theorem magma.free_semigroup.of_mul_assoc_left

added theorem magma.free_semigroup.of_mul_assoc_right

added inductive magma.free_semigroup.r

added def magma.free_semigroup

added def semigroup.free_monoid.lift

added theorem semigroup.free_monoid.lift_mul

added theorem semigroup.free_monoid.lift_of

added theorem semigroup.free_monoid.lift_one

added theorem semigroup.free_monoid.lift_unique

added def semigroup.free_monoid.map

added theorem semigroup.free_monoid.map_mul

added theorem semigroup.free_monoid.map_of

added def semigroup.free_monoid.of

added theorem semigroup.free_monoid.of_mul

added def semigroup.free_monoid