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

[Merged by Bors] - refactor(module/ordered): make ordered_semimodule a mixin#4719

Closed
kim-em wants to merge 5 commits intomasterfrom
ordered_semimodule_mixin
Closed

[Merged by Bors] - refactor(module/ordered): make ordered_semimodule a mixin#4719
kim-em wants to merge 5 commits intomasterfrom
ordered_semimodule_mixin

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Oct 20, 2020

Per @urkud's suggestion at #4683. This should avoid having to introduce a separate ordered_algebra class.

@kim-em kim-em mentioned this pull request Oct 20, 2020
Closed
2 tasks
@kim-em kim-em added the awaiting-review The author would like community review of the PR label Oct 20, 2020
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Oct 21, 2020 •
edited
Loading

LGTM, but let's wait for the linter.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 21, 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 added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 22, 2020
urkud
urkud reviewed Oct 22, 2020
View reviewed changes
src/analysis/convex/cone.lean Outdated
(S : convex_cone M) (h : ∀ x y : M, x ≤ y ↔ y - x ∈ S) : ordered_semimodule ℝ M :=
{ to_semimodule := ‹_›,
.. (show ordered_semimodule ℝ M, from ordered_semimodule.mk'
{ .. (show ordered_semimodule ℝ M, from ordered_semimodule.mk'
Copy link
Copy Markdown
Member

@urkud urkud Oct 22, 2020

Choose a reason for hiding this comment

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

The trick with .. was here to avoid marking this def as noncomputable. Please make it a lemma and use ordered_semimodule.mk' directly.

@github-actions 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 github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 30, 2020
@urkud urkud 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 Oct 30, 2020
jcommelin
jcommelin approved these changes Oct 30, 2020
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 Oct 30, 2020
bors bot pushed a commit that referenced this pull request Oct 30, 2020
@kim-em @urkud
refactor(module/ordered): make ordered_semimodule a mixin (#4719)
63c0dac 
Per @urkud's suggestion at #4683. This should avoid having to introduce a separate `ordered_algebra` class.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(module/ordered): make ordered_semimodule a mixin [Merged by Bors] - refactor(module/ordered): make ordered_semimodule a mixin Oct 30, 2020
@bors bors bot closed this Oct 30, 2020
@bors bors bot deleted the ordered_semimodule_mixin branch October 30, 2020 11:08
lecopivo pushed a commit to lecopivo/mathlib that referenced this pull request Oct 31, 2020
@kim-em @urkud
refactor(module/ordered): make ordered_semimodule a mixin (leanprover…
55db22a 
…-community#4719)

Per @urkud's suggestion at leanprover-community#4683. This should avoid having to introduce a separate `ordered_algebra` class.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

2 more reviewers

@urkud urkud urkud 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.

3 participants

@kim-em @jcommelin @urkud