[Merged by Bors] - feat: port Data.Complex.Basic#2718
[Merged by Bors] - feat: port Data.Complex.Basic#2718siddhartha-gadgil wants to merge 42 commits intomasterfrom
Conversation
siddhartha-gadgil
commented
Mar 8, 2023
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
|
The commit 04c7d61 fixes many All checks pass before and after this commit. |
Co-authored-by: Johan Commelin <johan@commelin.net>
…er-community/mathlib4 into port/Data.Complex.Basic
| constructor <;> | ||
| simp <;> | ||
| · first |ring1|ring_nf | ||
| instance commRing : CommRing ℂ := |
There was a problem hiding this comment.
This should probably have a porting note too, since the instance above does.
Mathlib/Data/Complex/Basic.lean
Outdated
| #align complex.conj_of_real Complex.conj_ofReal | ||
|
|
||
| @[simp] | ||
| theorem conj_i : conj i = -i := |
There was a problem hiding this comment.
This has got misaligned with edits.
|
|
||
| /-- The norm squared function. -/ | ||
| @[pp_nodot] | ||
| -- @[pp_nodot] |
| -- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑` | ||
| @[simp] |
There was a problem hiding this comment.
This sounds like a bug in norm_cast we need to fix.
Mathlib/Data/Complex/Basic.lean
Outdated
| theorem abs_le_abs_re_add_abs_im (z : ℂ) : abs z ≤ |z.re| + |z.im| := by | ||
| simpa [re_add_im] using abs.add_le z.re (z.im * I) | ||
| -- Porting note: probably should be golfed | ||
| theorem abs_le_abs_re_add_abs_im (z : ℂ) : Complex.abs z ≤ |z.re| + |z.im| := by | ||
| repeat (rw [← abs_ofReal]) | ||
| conv => | ||
| lhs | ||
| rw [← Complex.re_add_im z] | ||
| simpa [re_add_im] using Complex.abs.add_le z.re (z.im * i) |
There was a problem hiding this comment.
Can we instead try to work out why the old proof fails?
There was a problem hiding this comment.
Generally I attribute proofs being longer to my lack of skill with tactics.
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…er-community/mathlib4 into port/Data.Complex.Basic
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |