-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain
#4156
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.
I haven't looked at the big file yet... will do that later.
Thanks for doing this!
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 only looked at the big file, I will do the rest later :)
multiset.induction_on f | ||
(λ h, (ha.1 (associated_one_iff_is_unit.1 h)).elim) | ||
(λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p, | ||
have hs0 : s = 0, from classical.by_contradiction | ||
(λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in | ||
(hs q (by simp [hq])).2.1 $ | ||
(ha.2 ((p * ↑(u⁻¹)) * (s.erase q).prod) _ | ||
(by {rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons, multiset.cons_erase hq, | ||
mul_comm p _, mul_assoc, ← multiset.prod_cons, hu.symm, mul_comm, mul_assoc], | ||
simp, })).resolve_left $ | ||
mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left | ||
(hs p (multiset.mem_cons_self _ _)).2.1), | ||
⟨(by {clear _let_match; simp * at *}), hs0 ▸ rfl⟩⟩) | ||
(pfa.2) (pfa.1) |
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 expect this proof would be more readable if it's formatted in tactic-style. For example, the pfa.2 pfa.1
arguments at the end can stay with the function call if we make them the arguments to a refine
call at the start.
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.
While the proof is fresh in your mind you could even add a couple of comments saying what's going on. Christian Szegedy told me today that the machine learning people are desperate for comments in code.
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've made this a tactic proof, but I can't really say it's "fresh in my mind", because I didn't write the original and don't particularly understand it. I've added a docstring to the top because it took me a moment even to understand the statement.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
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 looks absolutely great to me. Many thanks for doing it!
multiset.induction_on f | ||
(λ h, (ha.1 (associated_one_iff_is_unit.1 h)).elim) | ||
(λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p, | ||
have hs0 : s = 0, from classical.by_contradiction | ||
(λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in | ||
(hs q (by simp [hq])).2.1 $ | ||
(ha.2 ((p * ↑(u⁻¹)) * (s.erase q).prod) _ | ||
(by {rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons, multiset.cons_erase hq, | ||
mul_comm p _, mul_assoc, ← multiset.prod_cons, hu.symm, mul_comm, mul_assoc], | ||
simp, })).resolve_left $ | ||
mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left | ||
(hs p (multiset.mem_cons_self _ _)).2.1), | ||
⟨(by {clear _let_match; simp * at *}), hs0 ▸ rfl⟩⟩) | ||
(pfa.2) (pfa.1) |
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.
While the proof is fresh in your mind you could even add a couple of comments saying what's going on. Christian Szegedy told me today that the machine learning people are desperate for comments in code.
Just to mention that there's this funny finiteness result Hey yeah I guess it's also true that if R is a UFD then so is mv_polynomial's over R with variables in an arbitrary type. |
Yeah, this is all that's needed other than Gauss's Lemma for showing that a polynomial ring over a UFD is a UFD. |
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.
Thank you so much for the changes! Just a few stylistic issues and it looks good to me.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
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
Co-authored-by: Johan Commelin <johan@commelin.net>
Hopefully fixing this merge conflict doesn't break anything. |
Thanks 🎉 bors merge |
…ctor of `unique_factorization_domain` (#4156) Refactors `unique_factorization_domain` to `unique_factorization_monoid` `unique_factorization_monoid` is a predicate `unique_factorization_monoid` now requires no additive/subtractive structure Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
unique_factorization_domain
unique_factorization_domain
Refactors
unique_factorization_domain
tounique_factorization_monoid
unique_factorization_monoid
is a predicateunique_factorization_monoid
now requires no additive/subtractive structure