Commit 2024-08-07 08:06 ad4663c3

View on Github →

feat: norm_num ext for Int.floor (#13647) I tried this a while ago in https://github.com/leanprover-community/mathlib/pull/16502; this is now just one of the handlers from that PR.

Estimated changes

Modified Mathlib/Data/Rat/Floor.lean

added def Rat.evalIntFloor

modified theorem Rat.floor_int_div_nat_eq_div

added theorem Rat.isInt_intFloor

added theorem Rat.isInt_intFloor_ofIsRat

added theorem Rat.isNat_intFloor

Modified test/norm_num_ext.lean