NatSqrt

📁 Source: Mathlib/Tactic/NormNum/NatSqrt.lean

Statistics

Metric	Count
Definitions evalNatSqrt, proveNatSqrt	2
Theorems isNat_sqrt, nat_sqrt_helper	2
Total	4

Tactic.NormNum

Definitions

Name	Category	Theorems
evalNatSqrt 📖	CompOp	—
proveNatSqrt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNat_sqrt 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	—	—
nat_sqrt_helper 📖	—	—	—	—	pow_two Nat.sqrt_add_eq' Nat.instAtLeastTwoHAddOfNat two_mul

---

← Back to Index