-
Notifications
You must be signed in to change notification settings - Fork 42
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proved QHat.rat_meet_zHat and QHat.rat_join_zHat. #161
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is great, but since you asked for feedback, here's some things I might change. Please don't let the wall of text demotivate you; I'm just hoping you might find my suggestions interesting.
And please also add |
Done. |
Ruben, I think your 2nd lemma gave an error... |
Thanks a lot for your work on this! Can you resolve the issues which have been dealt with so I can see what's going on? Sorry, I've been dealing with real life for most of this week but now I've got more time for FLT. |
I'll first check if the lean and mathlib versions are compatible. |
Seems like my local lean version is |
Hmm, something about |
Due to the mathlib bump, |
It seems I have fixed it. |
Just resolved a small merge conflict. |
There are many unresolved conversations. Can you resolve those which are now dealt with? Then it will be easier to see what's going on. |
Proved
QHat.rat_meet_zHat
andQHat.rat_join_zHat
.