-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - feat(ring_theory): factorize a non-unit into irreducible factors without multiplying a unit #13682
Conversation
multiset.prod_erase
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.
LGTM
If @eric-wieser has no further comments can I get a bors d+? |
Thanks! bors d+ |
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…out multiplying a unit (#13682) Used in https://proofassistants.stackexchange.com/a/1312/93. Also adds simp lemma `multiset.prod_erase` used in the main proof and the auto-generated additive version, which is immediately analogous to [list.prod_erase](https://leanprover-community.github.io/mathlib_docs/data/list/big_operators.html#list.prod_erase). Also removes some extraneous namespace prefix.
Pull request successfully merged into master. Build succeeded: |
+ Shorten the proof of `exists_irreducible_factor` using `well_founded.has_min` instead of `well_founded.fix`. + Remove use of `simp` in `induction_on_irreducible`; now a pure term-mode proof except for the classical instance. + Change the proof of `not_unit_iff_exists_factors_eq` (just added in [#13682](#13682)) to use induction. The new proof doesn't require the `multiset.prod_erase` introduced in [#13682](#13682), but is about as complex as the old one, so I might change it back if reviewers prefer.
Used in https://proofassistants.stackexchange.com/a/1312/93. Also adds simp lemma
multiset.prod_erase
used in the main proof and the auto-generated additive version, which is immediately analogous to list.prod_erase. Also removes some extraneous namespace prefix.