Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-28 11:54 ca95726e

View on Github →

feat(algebra/free) additive versions, docs. (#2755) https://github.com/leanprover-community/mathlib/issues/930

Estimated changes

added inductive free_add_magma
modified def free_magma.length
modified def free_magma.lift
modified theorem free_magma.lift_mul
modified theorem free_magma.lift_of
modified def free_magma.map
modified theorem free_magma.map_mul'
modified theorem free_magma.map_mul
modified theorem free_magma.map_of
modified theorem free_magma.map_pure
modified theorem free_magma.mul_bind
added theorem free_magma.mul_eq
modified theorem free_magma.mul_map_seq
modified theorem free_magma.mul_seq
modified theorem free_magma.pure_bind
modified theorem free_magma.pure_seq
deleted def free_magma.repr'
modified theorem free_magma.traverse_eq
modified theorem free_magma.traverse_mul'
modified theorem free_magma.traverse_mul
modified theorem free_magma.traverse_pure'
modified theorem free_magma.traverse_pure
modified def free_semigroup.lift'
modified theorem free_semigroup.lift_mul
modified theorem free_semigroup.lift_of
modified theorem free_semigroup.lift_of_mul
modified theorem free_semigroup.map_mul'
modified theorem free_semigroup.map_mul
modified theorem free_semigroup.map_of
modified theorem free_semigroup.map_pure
modified theorem free_semigroup.mul_bind
modified theorem free_semigroup.mul_map_seq
modified theorem free_semigroup.mul_seq
modified theorem free_semigroup.pure_bind
modified theorem free_semigroup.pure_seq
modified theorem free_semigroup.traverse_eq
modified theorem free_semigroup.traverse_mul
modified theorem magma.free_semigroup.map_of
modified inductive magma.free_semigroup.r