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 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
modified theorem punit.inv_eq
modified theorem punit.mul_eq
modified theorem punit.one_eq