Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 21:15 0bb0cec5

View on Github →

feat(group_theory): free_group and free_abelian_group are lawful monads (#737)

Estimated changes

Modified src/group_theory/free_abelian_group.lean

added theorem free_abelian_group.add_bind

added theorem free_abelian_group.add_seq

added theorem free_abelian_group.map_add

added theorem free_abelian_group.map_neg

added theorem free_abelian_group.map_pure

added theorem free_abelian_group.map_sub

added theorem free_abelian_group.map_zero

added theorem free_abelian_group.neg_bind

added theorem free_abelian_group.neg_seq

added theorem free_abelian_group.pure_bind

added theorem free_abelian_group.pure_seq

added theorem free_abelian_group.seq_add

added theorem free_abelian_group.seq_neg

added theorem free_abelian_group.seq_sub

added theorem free_abelian_group.seq_zero

added theorem free_abelian_group.sub_bind

added theorem free_abelian_group.sub_seq

added theorem free_abelian_group.zero_bind

added theorem free_abelian_group.zero_seq

Modified src/group_theory/free_group.lean

added theorem free_group.inv_bind

modified theorem free_group.map.comp

added theorem free_group.map_inv

added theorem free_group.map_mul

added theorem free_group.map_one

added theorem free_group.map_pure

added theorem free_group.mul_bind

added theorem free_group.one_bind

added theorem free_group.pure_bind

modified theorem free_group.quot_lift_mk

modified theorem free_group.quot_lift_on_mk

modified theorem free_group.to_group_eq_prod_map

modified def free_group