Commit 2022-11-07 21:34 baa48106

View on Github →

feat: norm_num addition on AddMonoidWithOne (#551) As requested on Zulip.

Estimated changes

Modified Mathlib/Tactic/NormNum/Basic.lean

modified theorem Mathlib.Meta.NormNum.isNat_add

modified theorem Mathlib.Meta.NormNum.isNat_cast

modified theorem Mathlib.Meta.NormNum.isNat_ofNat

modified theorem Mathlib.Meta.NormNum.isNat_one

modified theorem Mathlib.Meta.NormNum.isNat_zero

Modified Mathlib/Tactic/NormNum/Core.lean

modified theorem Mathlib.Meta.NormNum.IsNat.of_raw

modified theorem Mathlib.Meta.NormNum.IsNat.to_eq

modified theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq

modified structure Mathlib.Meta.NormNum.IsNat

added def Mathlib.Meta.NormNum.inferAddMonoidWithOne

added def Mathlib.Meta.NormNum.instAddMonoidWithOne

added def Mathlib.Meta.NormNum.instAddMonoidWithOneNat

deleted def Mathlib.Meta.NormNum.instSemiringNat

modified def Nat.rawCast

Modified Mathlib/Tactic/Ring.lean

Modified test/norm_num.lean