Commit 2022-12-26 11:29 e8ce8bcd

View on Github →

fix Data.Int.Basic: fix zsmul on ℤ (#1217) This way two instances for m • n, m n : ℤ, are defeq. Also use defeq to golf some proofs.

Estimated changes

added theorem Int.ofAdd_mul
deleted theorem Int.of_add_mul
added theorem Int.toAdd_pow
added theorem Int.toAdd_zpow
deleted theorem Int.to_add_pow
deleted theorem Int.to_add_zpow
added theorem Nat.ofAdd_mul
deleted theorem Nat.of_add_mul
added theorem Nat.toAdd_pow
deleted theorem Nat.to_add_pow