[Merged by Bors] - feat(data/complex): order structure by kim-em · Pull Request #4684 · leanprover-community/mathlib3

kim-em · 2020-10-19T10:46:50Z

depends on: [Merged by Bors] - feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 #4363
depends on: [Merged by Bors] - feat(algebra/algebra/ordered): ordered algebras #4683

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

…ro_le_one

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

…community/mathlib into ordered_semiring_zero_le_one

…ro_le_one

github-actions · 2021-01-07T13:49:39Z

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

kim-em · 2021-02-04T09:00:26Z

Hopefully this has been successfully raised from the dead.

dupuisf · 2021-02-05T01:09:33Z

If we add this instance, wouldn't it make more sense to do it via is_R_or_C...?

kim-em · 2021-02-05T02:02:47Z

If we add this instance, wouldn't it make more sense to do it via is_R_or_C...?

One objection is that R already has these structures, so if we provided an instance via is_R_or_C we might be adding confusingly duplicated instances.

Could you expand on why you think it would be useful to involve is_R_or_C here?

An alternative but more long term approach would be to wait until we have C*-algebras...

dupuisf · 2021-02-05T15:16:00Z

One objection is that R already has these structures, so if we provided an instance via is_R_or_C we might be adding confusingly duplicated instances.

Oh, right.

Could you expand on why you think it would be useful to involve is_R_or_C here?

The places I had in mind where I think it would make life easier tend to involve is_R_or_C, for example the proof of Cauchy-Schwarz in inner_product.lean. But yeah, it's probably easier to just summon [partial_order 𝕜] whenever this is needed.

src/data/complex/basic.lean

improvements to tactic proofs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/data/complex/basic.lean

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

bryangingechen

LGTM. Thanks!
bors r+

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

bors · 2021-02-11T20:20:52Z

Pull request successfully merged into master.

Build succeeded:

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

kim-em and others added 30 commits September 28, 2020 19:16

.

3eeb6cc

chore(algebra/ordered_ring): remove duplicate lemma

c130f01

merge

b33eef9

move some lemmas up

bde96cb

missed one

3da41fb

Merge branch 'two_pos' into ordered_semiring_zero_lt_one

8b5572c

merge

1e44000

Update src/algebra/ordered_ring.lean

d826c10

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Merge branch 'master' into ordered_semiring_zero_lt_one

36f304d

Update src/algebra/ordered_ring.lean

fe6d033

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

.

fd9f8f0

merge

c4ef103

Merge remote-tracking branch 'origin/master' into ordered_semiring_ze…

ece1c70

…ro_le_one

ugh, this is going to be tedious

528f9fa

ugh

8784384

builds

9d27d2d

minor

b42ed8a

merge

9d3033f

better tactic

a5c797a

Update src/logic/nontrivial.lean

f2eb085

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Apply suggestions from code review

b17270f

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

linting

f9efeb4

Merge branch 'ordered_semiring_zero_le_one' of github.com:leanprover-…

709e73c

…community/mathlib into ordered_semiring_zero_le_one

Merge remote-tracking branch 'origin/master' into ordered_semiring_ze…

4869f5f

…ro_le_one

feat(logic/nontrivial): a tactic to summon nontrivial instances

bb080d1

use tactic

de2538d

merge

953cc62

add examples in doc-string

e1d5f32

fix

9cffa4a

merge

2e47db1

kim-em added 3 commits October 21, 2020 09:59

use ordered_semimodule

95ac5c6

fix

9af04ab

Merge branch 'ordered_algebra2' into complex_ordered_ring

07675bc

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 27, 2020

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 7, 2021

merge master

2eeb963

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 4, 2021

fix

8e4c9d3

kim-em added the awaiting-review The author would like community review of the PR label Feb 4, 2021

bryangingechen reviewed Feb 6, 2021

View reviewed changes

Apply suggestions from code review

1b49379

improvements to tactic proofs Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

bryangingechen reviewed Feb 11, 2021

View reviewed changes

src/data/complex/basic.lean Outdated Show resolved Hide resolved

kim-em and others added 2 commits February 11, 2021 18:26

Update src/data/complex/basic.lean

b4d2e44

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

localize instances involving order structure on complex

b203bd0

bryangingechen approved these changes Feb 11, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Feb 11, 2021

bors bot pushed a commit that referenced this pull request Feb 11, 2021

feat(data/complex): order structure (#4684)

a557f8b

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

bors bot changed the title ~~feat(data/complex): order structure~~ [Merged by Bors] - feat(data/complex): order structure Feb 11, 2021

bors bot closed this Feb 11, 2021

bors bot deleted the complex_ordered_ring branch February 11, 2021 20:21

jcommelin pushed a commit that referenced this pull request Feb 11, 2021

feat(data/complex): order structure (#4684)

357d05f

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

b-mehta pushed a commit that referenced this pull request Apr 2, 2021

feat(data/complex): order structure (#4684)

03df536

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

eric-wieser mentioned this pull request Aug 8, 2023

[Merged by Bors] - chore(Data/Complex): move order to a separate file leanprover-community/mathlib4#6457

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/complex): order structure#4684

[Merged by Bors] - feat(data/complex): order structure#4684
kim-em wants to merge 70 commits intomasterfrom
complex_ordered_ring

kim-em commented Oct 19, 2020 •

edited by github-actions bot

Loading

Uh oh!

github-actions bot commented Jan 7, 2021

Uh oh!

kim-em commented Feb 4, 2021

Uh oh!

dupuisf commented Feb 5, 2021

Uh oh!

kim-em commented Feb 5, 2021

Uh oh!

dupuisf commented Feb 5, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bryangingechen left a comment

Uh oh!

bors bot commented Feb 11, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

kim-em commented Oct 19, 2020 • edited by github-actions bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 7, 2021

Uh oh!

kim-em commented Feb 4, 2021

Uh oh!

dupuisf commented Feb 5, 2021

Uh oh!

kim-em commented Feb 5, 2021

Uh oh!

dupuisf commented Feb 5, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

bors bot commented Feb 11, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

kim-em commented Oct 19, 2020 •

edited by github-actions bot

Loading