Theorem Tactic.NormNum.isNat_realSqrt

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/RealSqrt.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.NormNum.isNat_realSqrtView on Github →
2025-03-01 19:37
Mathlib/Tactic/NormNum/RealSqrt.lean
feat: `norm_num` extension for `Real.sqrt` and `NNReal.sqrt` (#21102) …
Added Tactic.NormNum.isNat_realSqrtView on Github →