feat(algebra/order/floor): The image of `floor`/`ceil` under an order ring hom

[YaelDillies]

⌊f a⌋ = ⌊a⌋, ⌈f a⌉ = ⌈a⌉ and similar for f a strictly monotone ring homomorphism.

---

• [ ] depends on: #16024

@eric-wieser, those are the lemmas I told you about a week ago.

I tried generalizing to require only monotone, but it looks like it's wrong. I started writing a counterexample on branch map_floor_counterexample.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16024~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests