Commit 2022-02-23 09:06 5be1724a

View on Github →

feat: AddMonoidWithOne, AddGroupWithOne (#206) Counterpart to leanprover-community/mathlib#12182. Solves the performance issues with polymorphic numerals from #177, as well as the diamonds with Nat. A noteworthy feature is that after importing mathlib, the coercion ℕ → ℤ changes from Int.ofNat to Nat.cast.

Estimated changes

added def Int.cast
added theorem Int.cast_negSucc
added theorem Int.cast_ofNat
added theorem Int.cast_one
added theorem Int.cast_zero
added def Nat.cast
added theorem Nat.cast_add
added theorem Nat.cast_ofNat
added theorem Nat.cast_one
added theorem Nat.cast_succ
added theorem Nat.cast_zero
added theorem Int.cast_Nat_cast
added theorem Int.cast_id
added theorem Int.ofNat_eq_cast
deleted theorem Nat.cast_Int
deleted theorem Nat.cast_Nat
deleted theorem Nat.cast_add
added theorem Nat.cast_id
modified theorem Nat.cast_mul
deleted theorem Nat.cast_one
modified theorem Nat.cast_pow
deleted theorem Nat.cast_succ'
deleted theorem Nat.cast_succ
deleted theorem Nat.cast_succ_succ
deleted theorem Nat.cast_zero
deleted theorem Nat.pow_succ'
added def Fin.ofInt'
added theorem Nat.Nat.pow_eq
added theorem Nat.Nat.pow_succ'