Skip to content

[Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier#6483

Closed
adomani wants to merge 1 commit intomasterfrom
adomani_eq_and_eq_of_le_of_le_of_add_le
Closed

[Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier#6483
adomani wants to merge 1 commit intomasterfrom
adomani_eq_and_eq_of_le_of_le_of_add_le

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented Aug 10, 2023

This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:

Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic

Open in Gitpod

@adomani adomani added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Aug 10, 2023
@adomani adomani mentioned this pull request Aug 10, 2023
Closed
1 task
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 10, 2023
ocfnash
ocfnash approved these changes Aug 10, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 10, 2023
bors bot pushed a commit that referenced this pull request Aug 10, 2023
@adomani
chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move `eq_an…
35ae770 
…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```
@bors
Copy link
Copy Markdown

bors bot commented Aug 10, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier [Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier Aug 10, 2023
@bors bors bot closed this Aug 10, 2023
@bors bors bot deleted the adomani_eq_and_eq_of_le_of_le_of_add_le branch August 10, 2023 10:11
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@adomani @kim-em
chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move `eq_an…
d6b9518 
…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@adomani @kim-em
chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move `eq_an…
1a063a8 
…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@adomani @ocfnash