Commit 2023-05-27 12:18 23055ecf

View on Github →

port: Nat.sqrt extension for norm_num (#4027)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NormNum/NatSqrt.lean

added def Tactic.NormNum.evalNatSqrt

added theorem Tactic.NormNum.isNat_sqrt

added theorem Tactic.NormNum.nat_sqrt_helper

added def Tactic.NormNum.proveNatSqrt

Modified test/norm_num_ext.lean