Mathlib Changelog
v4
Changelog
About
Github
Theorem
Tactic.NormNum.isRat_realSqrt_of_isRat_ofNat
Modification history
2025-08-13 09:12
Mathlib/Tactic/NormNum/RealSqrt.lean
refactor: Add norm_num machinery for NNRat (#9915) …
Deleted
Tactic.NormNum.isRat_realSqrt_of_isRat_ofNat
View 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.isRat_realSqrt_of_isRat_ofNat
View on Github →