[Merged by Bors] - feat(Data/Complex): add lemmas like re_eq_abs#8025
[Merged by Bors] - feat(Data/Complex): add lemmas like re_eq_abs#8025
re_eq_abs#8025Conversation
urkud
commented
Oct 30, 2023
Mathlib/Data/Complex/Basic.lean
Outdated
| not_iff_not.1 <| (abs_im_le_abs z).lt_iff_ne.symm.trans abs_im_lt_abs | ||
|
|
||
| @[simp] | ||
| lemma re_eq_abs {z : ℂ} : z.re = abs z ↔ 0 ≤ z.re ∧ z.im = 0 := |
There was a problem hiding this comment.
RHS of this lemma can be formulated as 0 ≤ z but that makes sense only if you open the ComplexOrder locale. Which form should I use? Similarly for the next two lemmas and z ≤ 0.
There was a problem hiding this comment.
My preference would be to open the ComplexOrder locale, and that we should do this whenever it allows use to phrase things naturally. If we have enough examples of it throughout the library, maybe people will see the value of having this as a global instance.
|
bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
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. |
re_eq_absre_eq_abs