Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-10 05:26 0f8a5c8d

View on Github →

refactor(algebra/group): Use a user attr for to_additive Parts of this commit are redundant pending leanprover/lean#1857 .

Estimated changes

modified theorem finset.prod_congr
modified theorem finset.prod_const_one
modified theorem finset.prod_empty
modified theorem finset.prod_image
modified theorem finset.prod_insert
modified theorem finset.prod_inv_distrib
modified theorem finset.prod_singleton
deleted theorem list.prod_append
deleted theorem list.prod_cons
deleted theorem list.prod_eq_of_perm
deleted theorem list.prod_join
deleted theorem list.prod_nil
deleted theorem list.prod_repeat
deleted theorem list.prod_reverse
modified theorem inv_eq_one
modified theorem inv_inj'
modified theorem inv_ne_one
modified theorem mul_left_inj
modified theorem mul_right_inj
modified theorem mul_self_iff_eq_one
added theorem list.prod_repeat
deleted theorem list.fold_op_eq_of_perm
deleted theorem list.foldl_assoc
deleted theorem list.map_congr
added theorem list.foldl_assoc
added theorem list.map_congr
added theorem list.prod_append
added theorem list.prod_cons
added theorem list.prod_join
added theorem list.prod_nil
deleted def list.sum
added theorem list.prod_eq_of_perm
added theorem list.prod_reverse
modified theorem nat.size_one