mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open YaelDillies opened this issue 3 years ago • 1 comments

⌊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.

Open in Gitpod

YaelDillies avatar Aug 12 '22 11:08 YaelDillies

This PR/issue depends on:

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

mathlib-dependent-issues-bot avatar Aug 21 '22 09:08 mathlib-dependent-issues-bot

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 24 '22 12:08 bors[bot]