Stream: Is there code for X?
Devon Tuma (Aug 14 2020 at 18:08):
I've found in
ring_theory/ideal/over.lean the statement
is_maximal_of_is_integral_of_is_maximal_comap, but I can't find a converse statement along the lines of
is_maximal_comap_of_is_integral_of_is_maximal, which is what I want. I would guess this doesn't exist yet since I'd expect it to be in the same file, but I wanted to double check I wasn't missing something before I try and write a proof myself.
Johan Commelin (Aug 14 2020 at 19:12):
@Anne Baanen Can you confirm?
But I guess it's true that we don't have this.
Johan Commelin (Aug 14 2020 at 19:13):
If someone wants to do going-up/going-down theorems, that would be nice! I think there are even comments about such a TODO in that file.
Devon Tuma (Aug 14 2020 at 20:41):
I could look at doing some of that then, it seems better than just ad-hoc proving the one statement I want, assuming no one else is already working on anything in that area.
Anne Baanen (Aug 15 2020 at 09:31):
That file was mostly me ad-hoc proving the statements that I needed. I would be very happy if you do (some of) going-up/going-down!
Last updated: May 17 2021 at 16:26 UTC