Def Tactic.NormNum.evalRatNum

Modification history

2026-07-16 01:47
Mathlib/Tactic/NormNum/GCD.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.NormNum.evalRatNumView on Github →
2024-11-19 17:06
Mathlib/Tactic/NormNum/GCD.lean
feat: `norm_num` extension for `Rat.num` and `Rat.den` (#19099) …
Added Tactic.NormNum.evalRatNumView on Github →