Commit 2021-11-30 17:06 ceae8916

View on Github →

refactor(Data/Int): move Int notation to separate file (#113)

  • Rename one_succ_zero -> one_eq_succ_zero
  • Declare ℤ notation in init
  • Minimize some imports

Estimated changes

added theorem Nat.one_eq_succ_zero
deleted theorem Nat.one_succ_zero