Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/algebra/ordered): ordered algebras#4683

Closed
kim-em wants to merge 65 commits intomasterfrom
ordered_algebra2
Closed

[Merged by Bors] - feat(algebra/algebra/ordered): ordered algebras#4683
kim-em wants to merge 65 commits intomasterfrom
ordered_algebra2

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Oct 19, 2020 •
edited by github-actions bot
Loading

An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring,
for which scalar multiplication is "compatible" with the two orders.

kim-em and others added 30 commits September 28, 2020 19:16
@kim-em
.
3eeb6cc
@kim-em
chore(algebra/ordered_ring): remove duplicate lemma
c130f01
@kim-em
merge
b33eef9
@kim-em
move some lemmas up
bde96cb
@kim-em
missed one
3da41fb
@kim-em
Merge branch 'two_pos' into ordered_semiring_zero_lt_one
8b5572c
@kim-em
merge
1e44000
@kim-em @gebner
Update src/algebra/ordered_ring.lean
d826c10 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@robertylewis
Merge branch 'master' into ordered_semiring_zero_lt_one
36f304d
@kim-em @gebner
Update src/algebra/ordered_ring.lean
fe6d033 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@kim-em
.
fd9f8f0
@kim-em
merge
c4ef103
@kim-em
Merge remote-tracking branch 'origin/master' into ordered_semiring_ze…
ece1c70 
…ro_le_one
@kim-em
ugh, this is going to be tedious
528f9fa
@kim-em
ugh
8784384
@kim-em
builds
9d27d2d
@kim-em
minor
b42ed8a
@kim-em
merge
9d3033f
@kim-em
better tactic
a5c797a
@kim-em @gebner
Update src/logic/nontrivial.lean
f2eb085 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@kim-em @gebner
Apply suggestions from code review
b17270f 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@kim-em
linting
f9efeb4
@kim-em
Merge branch 'ordered_semiring_zero_le_one' of github.com:leanprover-…
709e73c 
…community/mathlib into ordered_semiring_zero_le_one
@kim-em
Merge remote-tracking branch 'origin/master' into ordered_semiring_ze…
4869f5f 
…ro_le_one
@kim-em
feat(logic/nontrivial): a tactic to summon nontrivial instances
bb080d1
@kim-em
use tactic
de2538d
@kim-em
merge
953cc62
@kim-em
add examples in doc-string
e1d5f32
@kim-em
fix
9cffa4a
@kim-em
merge
2e47db1
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 12, 2020
@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Nov 13, 2020
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 14, 2020

Still some linter unhappiness

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 14, 2020
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 14, 2020

bors d+ jalex-stark

@bors
Copy link
Copy Markdown

bors bot commented Nov 14, 2020

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin jcommelin removed the awaiting-review The author would like community review of the PR label Nov 14, 2020
@bryangingechen
Copy link
Copy Markdown
Collaborator

bryangingechen commented Nov 14, 2020

let's see if this works?
bors d=[jalex-stark]

@bryangingechen bryangingechen added the delegated The PR author may merge after reviewing final suggestions. label Nov 14, 2020
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 17, 2020

bors d=jalex-stark

@bors
Copy link
Copy Markdown

bors bot commented Nov 17, 2020

✌️ jalex-stark can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 17, 2020

Hooray! I succesfully managed to convey my intent to a piece of rusty metal!

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 9, 2020

🎉 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!

@bryangingechen
Copy link
Copy Markdown
Collaborator

bryangingechen commented Jan 3, 2021

@jcommelin I fixed the lint but couldn't resist making a bunch of formatting changes in analysis/convex/basic.lean. Can we still merge? 😉

@bryangingechen bryangingechen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 6, 2021
@bryangingechen bryangingechen requested a review from urkud January 6, 2021 00:14
jcommelin
jcommelin approved these changes Jan 7, 2021
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions 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 Jan 7, 2021
bors bot pushed a commit that referenced this pull request Jan 7, 2021
@kim-em @robertylewis
feat(algebra/algebra/ordered): ordered algebras (#4683)
2c8175f 
An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring,
for which scalar multiplication is "compatible" with the two orders.



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

bors bot commented Jan 7, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/algebra/ordered): ordered algebras [Merged by Bors] - feat(algebra/algebra/ordered): ordered algebras Jan 7, 2021
@bors bors bot closed this Jan 7, 2021
@bors bors bot deleted the ordered_algebra2 branch January 7, 2021 13:08
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@urkud urkud Awaiting requested review from urkud

2 more reviewers

@kbuzzard kbuzzard kbuzzard left review comments

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@kim-em @urkud @jcommelin @bryangingechen @kbuzzard @fpvandoorn @robertylewis @jalex-stark