Commit 2025-09-23 14:25 c73c039b

View on Github →

feat: norm_num extension for abs (#29223) Adds a norm_num extension for the absolute value operator.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/ExponentialBounds.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/NormNum.lean

Created Mathlib/Tactic/NormNum/Abs.lean

added def Mathlib.Meta.NormNum.evalAbs

added theorem Mathlib.Meta.NormNum.isNNRat_abs_neg

added theorem Mathlib.Meta.NormNum.isNNRat_abs_nonneg

added theorem Mathlib.Meta.NormNum.isNat_abs_neg

added theorem Mathlib.Meta.NormNum.isNat_abs_nonneg

Created MathlibTest/norm_num_abs.lean