Commit 2025-11-05 04:06 7a71f834

View on Github →

feat: add norm_num extensions (#28836) Add norm_num extensions for

Int.negOfNat;
Nat.floor, Nat.ceil, and Int.round.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Semifield.lean

added theorem Mathlib.Meta.NormNum.IsInt.natFloor

added theorem Mathlib.Meta.NormNum.IsNNRat.natFloor

added theorem Mathlib.Meta.NormNum.IsNat.natFloor

added theorem Mathlib.Meta.NormNum.IsRat.natFloor

added def Mathlib.Meta.NormNum.evalNatFloor

Modified Mathlib/Data/NNRat/Floor.lean

added theorem Mathlib.Meta.NormNum.IsInt.natCeil

added theorem Mathlib.Meta.NormNum.IsNNRat.natCeil

added theorem Mathlib.Meta.NormNum.IsNat.natCeil

added theorem Mathlib.Meta.NormNum.IsRat.natCeil

added def Mathlib.Meta.NormNum.evalNatCeil

Modified Mathlib/Data/Rat/Floor.lean

added theorem Rat.IsRat.isInt_round

added def Rat.evalRound

added theorem Rat.isInt_round

added theorem Rat.isNat_round

Modified Mathlib/Tactic/NormNum/Basic.lean

added def Mathlib.Meta.NormNum.evalNegOfNat

added theorem Mathlib.Meta.NormNum.isInt_negOfNat

Modified MathlibTest/norm_num_ext.lean