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

feat: more mul lemmas for Nat #198

Merged
merged 5 commits into from
Jan 11, 2024
Merged

feat: more mul lemmas for Nat #198

merged 5 commits into from
Jan 11, 2024

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Jul 23, 2023 •
edited
Loading

The major changes here are deprecating lemmas with obscure names: Nat.mul_le_mul_of_nonneg_left, Nat.mul_le_mul_of_nonneg_right, Nat.mul_lt_mul, Nat.mul_lt_mul'.

This PR also finally implements #118 as Nat.mul_lt_mul_of_lt_of_lt.

@fgdorais fgdorais mentioned this pull request Jul 23, 2023
Closed
3 tasks
@fgdorais fgdorais force-pushed the nat-mul branch 2 times, most recently from 76451bb to d8834f8 Compare July 24, 2023 14:09
@fgdorais fgdorais mentioned this pull request Jul 28, 2023
Closed
1 task
@fgdorais fgdorais added the awaiting-author Waiting for PR author to address issues label Aug 21, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 19, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 1, 2023
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Nov 1, 2023
digama0
digama0 reviewed Nov 1, 2023
View reviewed changes
digama0
digama0 reviewed Nov 1, 2023
View reviewed changes
digama0
digama0 reviewed Nov 1, 2023
View reviewed changes
@digama0 digama0 added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Nov 1, 2023
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Nov 2, 2023
@fgdorais
feat: more mul lemmas for Nat
79f7ebf 
Potentially breaking:

* Deprecated `Nat.mul_le_mul_of_nonneg_left`.
* Deprecated `Nat.mul_le_mul_of_nonneg_right`.
* Deprecated `Nat.mul_lt_mul`.
* Deprecated `Nat.mul_lt_mul'`.
* Some implicit parameters may have been renamed or reordered.
@fgdorais
fix: remove deprecated section
c10f82e
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 28, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 9, 2023
@fgdorais fgdorais added WIP work in progress and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Dec 9, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 10, 2023
@fgdorais fgdorais removed the WIP work in progress label Dec 10, 2023
@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 10, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 10, 2023
@joehendrix joehendrix requested a review from kim-em January 10, 2024 22:48
@kim-em
Copy link
Collaborator

kim-em commented Jan 11, 2024

(Joe asked that I merge this after reviewing; I'm happy now, so about to hit merge.)

@kim-em kim-em merged commit 0b2e962 into leanprover-community:main Jan 11, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kim-em kim-em kim-em left review comments

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@fgdorais @kim-em @eric-wieser @digama0 @leanprover-community-mathlib4-bot