[Merged by Bors] - feat(ring_theory/localization/away) : Add num_denom section
#18830
Conversation
faenuccio
added
awaiting-review
| variables [is_domain R] [normalization_monoid R] [unique_factorization_monoid R] | ||
| include hx | ||
|
|
||
| lemma max_power_factor {a₀ : R} (h : a₀ ≠ 0) [nontrivial R] : |
There was a problem hiding this comment.
Can you move this to unique_factorization_domain.lean? (Or perhaps add a remark to do so after the port?)
There was a problem hiding this comment.
Do you mean just this lemma max_power_factor or all the additions?
There was a problem hiding this comment.
Just this lemma, since it doesn't assume anything about localizations, right?
There was a problem hiding this comment.
I have moved max_power_factor to unique _factorization_domain and I have opened the corresponding PR in mathlib4 3558.
Vierkantor
added
awaiting-author
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
faenuccio
added
awaiting-review
YaelDillies
changed the title
num_denom section
github-actions
bot
added
the
modifies-synchronized-file
faenuccio
added
WIP
|
I have closed all goals, and commented all the stuff relative to the old version using |
There was a problem hiding this comment.
Thank you for your work and your patience in the past days! I think we're nearly there, just a few steps:
- address my suggestion
- fix the linting errors
- delete commented-out (or otherwise unused code)
If the above steps went straightforwardly, then please feel free to bors merge this yourself.
bors d+
|
✌️ faenuccio can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors merge |
|
👎 Rejected by label |
faenuccio
removed
WIP
|
bors r+ |
Added a section `num_denom`: the main result is the lemma `exists_reduced_fraction` that shows that every non-zero element `b` in a `localization.away x` of a UFM can be written in a unique way as `b=x^n * a` with `n : ℤ` and `a` not divisible by `x`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
num_denom sectionnum_denom section
…tor` as in #18830 (#3558) Add lemma `max_powerFactor` needed in leanprover-community/mathlib#18830 and modified there.
Added a section
num_denom: the main result is the lemmaexists_reduced_fractionthat shows that every non-zero elementbin alocalization.away xof a UFM can be written in a unique way asb=x^n * awithn : ℤandanot divisible byx.