[Merged by Bors] - feat (RingTheory/Valuation/Integers) : add lemma one_of_isUnit' #12247
Conversation
faenuccio
added
awaiting-review
| @@ -76,6 +76,14 @@ theorem one_of_isUnit {x : O} (hx : IsUnit x) : v (algebraMap O R x) = 1 := | |||
| exact mul_le_mul_left' (hv.2 (u⁻¹ : Units O)) _ | |||
| #align valuation.integers.one_of_is_unit Valuation.Integers.one_of_isUnit | |||
|
|
|||
| theorem one_of_isUnit' {x : O} (hx : IsUnit x) (H : ∀ x, v (algebraMap O R x) ≤ 1) : | |||
There was a problem hiding this comment.
Am I correct that this does not use (hv : Integers v O)? Since it is not immediate to see what hypotheses are included or not, maybe use this to golf one_of_isUnit or add a docstring or move it out of the Integers namespace instead to make It clearer?
There was a problem hiding this comment.
You are certainly right, but since this is never needed when you #check it the variable hv does not show up. I have at any rate followed your suggestion and simplified the proof of one_of_isUnit.
erdOne
added
awaiting-author
faenuccio
added
awaiting-review
|
@erdOne Did you find the time to have another look at my modifications following your suggestions? |
|
Oops didn't notice that this is ready for review again. Thanks for the ping. |
|
🚀 Pull request has been placed on the maintainer queue by erdOne. |
|
bors merge |
github-actions
bot
added
ready-to-merge
Add lemma `one_of_isUnit'` , that is a generalization of `one_of_isUnit` with a slightly weaker assumption. Co-authored-by: María Inés de Frutos Fernández @mariainesdff
Thanks ;-) |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Add lemma `one_of_isUnit'` , that is a generalization of `one_of_isUnit` with a slightly weaker assumption. Co-authored-by: María Inés de Frutos Fernández @mariainesdff
Add lemma `one_of_isUnit'` , that is a generalization of `one_of_isUnit` with a slightly weaker assumption. Co-authored-by: María Inés de Frutos Fernández @mariainesdff
Add lemma
one_of_isUnit', that is a generalization ofone_of_isUnitwith a slightly weaker assumption.Co-authored-by: María Inés de Frutos Fernández @mariainesdff