Theorem Mathlib.Meta.NormNum.isNat_realSqrt_of_isRat_negOfNat

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/RealSqrt.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Added Mathlib.Meta.NormNum.isNat_realSqrt_of_isRat_negOfNatView on Github →