Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-22 21:15 7f103fd3

View on Github →

fix(tactic/transport): make to_additive copy protectedstatus (#2212)

  • fix(tactic/transport): make to_additive copy protectedstatus Fixes #2210, also slightly cleanup algebra/group/units
  • Fix compile (protected finset.sum)
  • Fix usage of finset.sum
  • Update src/tactic/transport.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
  • fix build

Estimated changes

deleted theorem nat.add_units_eq_one
added theorem nat.add_units_eq_zero