Theorem Tactic.NormNum.irrational_sqrt_rat_of_num

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/Irrational.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.NormNum.irrational_sqrt_rat_of_numView on Github →
2026-04-09 14:18
Mathlib/Tactic/NormNum/Irrational.lean
fix: some norm_num exts are not available in the module system (#37820) …
Added Tactic.NormNum.irrational_sqrt_rat_of_numView on Github →