Skip to content

[Merged by Bors] - chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m#9505

Closed
YaelDillies wants to merge 3 commits intomasterfrom
move_pow_eq_pow
Closed

[Merged by Bors] - chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m#9505
YaelDillies wants to merge 3 commits intomasterfrom
move_pow_eq_pow

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jan 7, 2024

Those lemmas were very recently added in #9397. Also make them iffs and golf.

Part of #9411

Open in Gitpod

@YaelDillies
chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
bcd60b6 
Those lemmas were very recently added in #9397. Also make them iffs and golf.

Part of #9411
@YaelDillies YaelDillies added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jan 7, 2024
@YaelDillies YaelDillies mentioned this pull request Jan 7, 2024
Closed
21 tasks
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jan 7, 2024

I think these make more sense in Mathlib/Algebra/GroupWithZero/Power.lean than in Mathlib/Data/Int/GCD.lean? Or are you planning on removing the former as well?

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jan 7, 2024

Algebra.GroupWithZero.Power is purely about algebraic properties of pow and zpow. Your results use gcd properties, hence are more number theoretic in flavor.

You could put them in Algebra.GroupWithZero.Power because that file has overinflated imports due to importing Algebra.GroupPower.Lemmas which is a mess of imports.

I noticed it when I merged master in #9411, since your proof was suddenly missing imports. I added the assert_not_exists Set.range clause which is already effective in most of the algebraic hierarchy and tried to add imports back to make your proofs compile, but that wasn't possible since your last statement mentions Set.range.

I also do not exclude removing Algebra.GroupWithZero.Power eventually, since it's already supposed to be covered by the files in Algebra.GroupPower.

jcommelin
jcommelin approved these changes Jan 8, 2024
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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 8, 2024
@YaelDillies
chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m (#9505)
006e9a3 
Those lemmas were very recently added in #9397. Also make them iffs and golf.

Part of #9411
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m [Merged by Bors] - chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m Jan 8, 2024
@mathlib-bors mathlib-bors bot closed this Jan 8, 2024
@mathlib-bors mathlib-bors bot deleted the move_pow_eq_pow branch January 8, 2024 13:15
mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2024
@YaelDillies
refactor: Delete Algebra.GroupPower.Lemmas (#9411)
8b4653a 
`Algebra.GroupPower.Lemmas` used to be a big bag of lemmas that made it there on the criterion that they needed "more imports". This was completely untrue, as all lemmas could be moved to earlier files in PRs:
- #9440
- #9442
- #9443
- #9455
- #9456
- #9457
- #9459
- #9461
- #9463
- #9466
- #9501
- #9502
- #9503
- #9505
- #9551
- #9553
- #9720
- #9739
- #9740
- #9805
- #9806
- and this one

There are several reasons for this:
* Necessary lemmas have been moved to earlier files since lemmas were dumped in `Algebra.GroupPower.Lemmas`
* In the Lean 3 → Lean 4 transition, Std acquired basic `Int` and `Nat` lemmas which let us shortcircuit the part of the algebraic order hierarchy on which the corresponding general lemmas rest
* Some proofs were overpowered
* Some earlier files were tangled and I have untangled them

This PR finishes the job by moving the last few lemmas out of `Algebra.GroupPower.Lemmas`, which is therefore deleted.
mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2024
@YaelDillies
refactor: Delete Algebra.GroupPower.Lemmas (#9411)
6eb43dc 
`Algebra.GroupPower.Lemmas` used to be a big bag of lemmas that made it there on the criterion that they needed "more imports". This was completely untrue, as all lemmas could be moved to earlier files in PRs:
- #9440
- #9442
- #9443
- #9455
- #9456
- #9457
- #9459
- #9461
- #9463
- #9466
- #9501
- #9502
- #9503
- #9505
- #9551
- #9553
- #9720
- #9739
- #9740
- #9805
- #9806
- and this one

There are several reasons for this:
* Necessary lemmas have been moved to earlier files since lemmas were dumped in `Algebra.GroupPower.Lemmas`
* In the Lean 3 → Lean 4 transition, Std acquired basic `Int` and `Nat` lemmas which let us shortcircuit the part of the algebraic order hierarchy on which the corresponding general lemmas rest
* Some proofs were overpowered
* Some earlier files were tangled and I have untangled them

This PR finishes the job by moving the last few lemmas out of `Algebra.GroupPower.Lemmas`, which is therefore deleted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

3 participants

@YaelDillies @erdOne @jcommelin