Commit 2021-09-24 22:20 5fbb5bb7

View on Github →

refactor(Tactic/NormNum): change to isNat function (#49)

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Ring/Basic.lean

modified theorem Nat.ofNat_eq_Nat

Modified Mathlib/Tactic/NormNum.lean

added def Lean.Meta.NormNum.evalEq

added theorem Lean.Meta.NormNum.eval_eq_of_isNat

added theorem Lean.Meta.NormNum.eval_of_isNat

added def Lean.Meta.NormNum.instSemiringNat

added def Lean.Meta.NormNum.isNat

added theorem Lean.Meta.NormNum.isNat_add

added theorem Lean.Meta.NormNum.isNat_mul

added theorem Lean.Meta.NormNum.isNat_pow

added theorem Lean.Meta.NormNum.isNat_rawNat

deleted theorem Lean.Meta.NormNum.ofNat_add

deleted theorem Lean.Meta.NormNum.ofNat_mul

deleted theorem Lean.Meta.NormNum.ofNat_nat

deleted theorem Lean.Meta.NormNum.ofNat_pow