Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-21 05:42 c5128756

View on Github →

refactor(*): rewrite to_additive attribute (#1345)

  • chore(algebra/group/to_additive): auto add structure fields
  • Snapshot
  • Rewrite @[to_additive]
  • Drop more explicit name arguments to to_additive
  • Drop more explicit arguments to to_additive
  • Map namespaces with run_cmd to_additive.map_namespace
  • fix(group_theory/perm/sign): fix compile
  • Fix handling of equational lemmas; fix warnings
  • Use list.mmap'

Estimated changes

deleted theorem finset.sum_hom
deleted theorem is_group_hom.finset_prod
deleted def add_monoid_hom.comp
deleted def add_monoid_hom.ext
deleted def add_monoid_hom.id
deleted theorem add_monoid_hom.map_neg
modified theorem add_monoid_hom.map_sub
deleted def add_monoid_hom.mk'
deleted def add_monoid_hom.neg
modified theorem coe_as_monoid_hom
added theorem monoid_hom.ext
deleted def monoid_hom.ext
deleted theorem monoid_hom.map_div
modified theorem monoid_hom.map_inv
modified theorem monoid_hom.map_mul
added theorem monoid_hom.map_mul_inv
modified theorem monoid_hom.map_one
added structure to_additive.value_type
modified theorem punit.inv_eq
modified theorem punit.mul_eq
modified theorem punit.one_eq
deleted def add_equiv.map_add
deleted def add_equiv.map_zero
deleted def add_equiv.refl
deleted def add_equiv.symm
deleted theorem add_equiv.to_equiv_symm
deleted def add_equiv.trans
modified def mul_equiv.map_one
modified def mul_equiv.refl
modified def mul_equiv.symm
modified theorem mul_equiv.to_equiv_symm
modified def mul_equiv.trans
modified theorem quotient_group.coe_inv
modified theorem quotient_group.coe_mul
modified theorem quotient_group.coe_one
modified theorem quotient_group.ker_mk
modified theorem quotient_group.lift_mk'
modified theorem quotient_group.lift_mk
deleted def add_group.closure
deleted theorem add_group.closure_subset
deleted theorem add_group.image_closure
added inductive add_group.in_closure
deleted theorem add_group.mem_closure
added theorem gmultiples_subset
added theorem gpowers_subset
modified theorem group.closure_subgroup
modified theorem is_subgroup.mem_trivial
deleted def add_monoid.closure
deleted theorem add_monoid.closure_mono
deleted theorem add_monoid.closure_subset
deleted theorem add_monoid.image_closure
added inductive add_monoid.in_closure
deleted theorem add_monoid.subset_closure
added theorem multiples.add_mem
added theorem powers.mul_mem
added def name.map_prefix
deleted theorem open_add_subgroup.coe_inf
deleted theorem open_add_subgroup.le_iff
modified theorem open_subgroup.coe_inf
modified theorem open_subgroup.le_iff