Commit 2024-11-19 17:06 22229e91

View on Github →

feat: norm_num extension for Rat.num and Rat.den (#19099) Closes #18826

Estimated changes

Modified Mathlib/Tactic/NormNum/GCD.lean

added def Tactic.NormNum.evalRatDen

added def Tactic.NormNum.evalRatNum

added theorem Tactic.NormNum.isInt_ratNum

added theorem Tactic.NormNum.isNat_ratDen

Modified MathlibTest/norm_num_ext.lean