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
refactor(algebra/field): partially migrate to bundled homs #1999
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.
Thanks for the work. Looks pretty good to me. Some minor questions.
λ x0 h, one_ne_zero $ calc | ||
1 = f (x * x⁻¹) : by rw [mul_inv_cancel x0, map_one f] | ||
... = 0 : by rw [map_mul f, h, zero_mul]⟩ | ||
⟨mt $ λ h, h.symm ▸ f.map_zero, |
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.
Should all these map_*
lemmas be simp
?
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.
I don't know. I guess they were not marked as simp
because looking for is_ring_hom
is expensive.
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.
So now, when we bundle, we can (and should?)
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.
Added some @[simp]
attrs.
|
||
lemma map_div' (h : y ≠ 0) : f (x / y) = f x / f y := | ||
(map_mul f).trans $ congr_arg _ $ map_inv' f h | ||
(f.map_mul _ _).trans $ congr_arg _ $ f.map_inv' h |
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.
@digama0 Is it time to make changes to Lean core, and fix the definition of field and division ring?
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.
Fine with me, although I would prefer to delegate the scheduling of the first non-backward compatible lean release to @robertylewis and @cipher1024 .
…r-community#1999) * refactor(algebra/field): partially migrate to bundled homs * Add a few `@[simp]` attrs Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…r-community#1999) * refactor(algebra/field): partially migrate to bundled homs * Add a few `@[simp]` attrs Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
TO CONTRIBUTORS:
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