Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Data.Complex.Exponential #2785

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat: port Data.Complex.Exponential #2785

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
7a0fe7a
feat: port Data.Complex.Exponential
ChrisHughes24 Mar 10, 2023
2152781
Initial file copy from mathport
ChrisHughes24 Mar 10, 2023
ae8ba38
automated fixes
ChrisHughes24 Mar 10, 2023
3aef49b
minor fix to Complex.Basic
ChrisHughes24 Mar 10, 2023
e619681
fix build
ChrisHughes24 Mar 10, 2023
7515dea
start work
ChrisHughes24 Mar 10, 2023
15350fd
fix some names
ChrisHughes24 Mar 10, 2023
a5cded8
progress
ChrisHughes24 Mar 10, 2023
3c23fa1
stuck at buggy lean
ChrisHughes24 Mar 10, 2023
17f691f
minor improvements
ChrisHughes24 Mar 10, 2023
0c4d753
prove ofReal_ofNat
ChrisHughes24 Mar 11, 2023
974c27b
Merge remote-tracking branch 'origin/master' into port/Data.Complex.E…
ChrisHughes24 Mar 11, 2023
e393967
slight tidy
ChrisHughes24 Mar 11, 2023
0325399
mild fixes
LukasMias Mar 12, 2023
eb8cfe7
Fixed exp_bound'
qawbecrdtey Mar 13, 2023
1351113
Indent fix.
qawbecrdtey Mar 13, 2023
53398c8
Fixed one_sub_le_exp_minus_of_pos
qawbecrdtey Mar 13, 2023
2cf9b2e
Fixed exp_bound_div_one_sub_of_interval
qawbecrdtey Mar 13, 2023
d5526e7
Merge remote-tracking branch 'origin/master' into port/Data.Complex.E…
ChrisHughes24 Mar 13, 2023
5b76f9b
small fixes
ChrisHughes24 Mar 13, 2023
f3717a6
more fixes
ChrisHughes24 Mar 13, 2023
ed9c891
fix build
ChrisHughes24 Mar 13, 2023
ac5fd49
fix lint
ChrisHughes24 Mar 13, 2023
24ecaf4
line length
ChrisHughes24 Mar 13, 2023
218da65
implement Real.exp positivity extenstion
dwrensha Mar 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -496,6 +496,7 @@ import Mathlib.Data.Bundle
import Mathlib.Data.ByteArray
import Mathlib.Data.Char
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Data.Countable.Basic
import Mathlib.Data.Countable.Defs
import Mathlib.Data.Countable.Small
Expand Down
8 changes: 8 additions & 0 deletions Mathlib/Data/Complex/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -483,6 +483,14 @@ set_option linter.uppercaseLean3 false in
theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ((OfNat.ofNat n : ℝ) : ℂ) = OfNat.ofNat n :=
rfl

@[simp]
theorem re_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n : ℂ).re = OfNat.ofNat n :=
rfl

@[simp]
theorem im_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n : ℂ).im = 0 :=
rfl

end
/-! ### Complex conjugation -/

Expand Down