damiano
damiano
Sure, but those lemmas involve inequalities on the non-lex type, which does not have an order currently.
Eric, thanks! I was missing the import! I added `lt/strict_order` instances as well. I copied over some of the `pi.lex` lemmas. I omitted the `bot` ones, since the instances for...
> Don't forget the lemmas `finsupp.to_lex_apply` and `finsupp.of_lex_apply`! These lemmas are in! I tried to use the `linear_order.lift`, but failed. If I understand your suggestion correctly, I was trying to...
@eric-wieser, if you are happy with this version feel free to push it! I am partly in favour of `wit` since it is a common way of arguing: you want...
@eric-wieser, do you mind if I PR the `finset.lattice` lemmas separately? I am about to open a PR with a proof of covariance that does not use `wit` (and is...
This PR has been essentially replaced by #16127.
Actually, I am now trying out to remove duplicate lemmas from `algebra.order.ring` and i think that the guiding principle should be that the order of explicit assumptions in this file...
Here is how I view this. Changing the order of hypotheses in "well-established" lemmas (e.g. the lemmas in `algebra.order.ring`) is something which involves touching a lot of files for a...
I agree that the lemmas where `0` and `1` both appear are still work in progress. However, the `zero_le_one` class was introduced very recently, and there were some doubts as...
@jcommelin, yes, this PR was waiting for the now-merged @16189.