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
doc(data/padics, data/real/cau_seq, algebra): add doc strings, remove unnecessary assumptions #1283
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 seems to sit on top of your doc PR for the padics. Is that intentional?
It's a general "cleanup" PR, I figured I might as well do it all together. (This is it, no more coming.) |
Ok, I see. Well, I guess we can merge it as soon as Travis confirms that you didn't clean up too much. |
Okay, this version definitely builds (and fixes a cascade of unnecessary arguments). |
Thanks @sgouezel , good catch! Updated. |
… unnecessary assumptions (leanprover-community#1283) * doc(data/padics): add doc strings, remove unnecessary prime assumptions * fix(data/real/cau_seq): remove unnecessary hypotheses * fix(algebra/{field, ordered_field}): remove unused assumptions * doc(data/real/cau_seq): document Cauchy sequences * fix(algebra/field): remove obsolete lemma * fix build * fix build * more unnecessary arguments * Update src/data/padics/padic_numbers.lean * Update src/data/padics/padic_numbers.lean * remove another unnecessary argument (suggested by @sgouezel)
This fixes a few declarations from #1282 (as well as one that didn't show up on that list for some reason), and adds documentation as per #1260 .
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list