Commit 2025-10-20 21:55 7468d44e

View on Github →

feat: norm_num support for Int.fract (#26428)

Estimated changes

Modified Mathlib/Data/Rat/Floor.lean

added def Rat.evalIntFract

added theorem Rat.isNNRat_intFract_of_isNNRat

added theorem Rat.isNat_intFract_of_isInt

added theorem Rat.isNat_intFract_of_isNat

added theorem Rat.isRat_intFract_of_isRat_negOfNat

Modified MathlibTest/norm_num_ext.lean