Commit 2025-06-24 02:04 20584e89

View on Github →

feat: norm_num plugin for Nat.clog (#26317)

Estimated changes

Modified Mathlib/Tactic/NormNum/NatLog.lean

added def Mathlib.Meta.NormNum.evalNatClog

added theorem Mathlib.Meta.NormNum.nat_clog_helper

added def Mathlib.Meta.NormNum.proveNatClog

Modified MathlibTest/norm_num_ext.lean