[Merged by Bors] - feat: norm_num ext for Int.floor

[eric-wieser]

I tried this a while ago in leanprover-community/mathlib3#16502; this is now just one of the handlers from that PR.

---

Some questions:

• Should these be in the NormNum/ directory?
• Are the isFoo lemmas supposed to be in the Mathlib.Meta.NormNum namespace?
• Is there any point in the isNat and isInt handlers, since simp can already deal with these?
• Do I really need CharZero?

[github-actions]

PR summary ddb5680aa4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ evalIntFloor
+ isInt_intFloor
+ isInt_intFloor_ofIsRat
+ isNat_intFloor

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[YaelDillies]

As mentioned on Zulip, this CharZero requirement comes for free once you import Algebra.Order.Ring.CharZero. I really dislike for basic inheritance typeclasses to be hidden in obscure files, so I have opened #13654.

[YaelDillies]

Can you merge master now that #13654 has landed?

[eric-wieser]

Done

[fpvandoorn]

Marking as awaiting-author. Please replace that label with awaiting-review if appropriate.

[YaelDillies]

Looking good!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[fpvandoorn]

Thanks!

bors merge

The versions for ceiling and nat-floor/nat-ceil would also be great!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style