[Merged by Bors] - chore: Delete Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise#11855
Closed
YaelDillies wants to merge 35 commits intomasterfrom
Closed
[Merged by Bors] - chore: Delete Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise#11855YaelDillies wants to merge 35 commits intomasterfrom
Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise#11855YaelDillies wants to merge 35 commits intomasterfrom
Conversation
The entire `Algebra.GroupPower` folder is problematic in that it treats `pow` as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of `pow` transversally. This PR scatters the lemmas in `Algebra.GroupPower.Basic` to earlier files. See #9411 for previous work.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
16 tasks
Contributor
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
This is quite big. Would you consider at least splitting out the removals from the moved code?
| theorem Odd.neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n := by | ||
| obtain ⟨k, rfl⟩ := h.exists_bit1 | ||
| exact zpow_bit1_neg _ _ | ||
| have hn : n ≠ 0 := by rintro rfl; exact Int.odd_iff_not_even.1 h even_zero |
Contributor
There was a problem hiding this comment.
This should exist as a lemma, IMO
| section | ||
| set_option linter.deprecated false | ||
| @[simp] | ||
| theorem I_zpow_bit0 (n : ℤ) : I ^ bit0 n = (-1 : ℂ) ^ n := by rw [zpow_bit0', I_mul_I] |
Contributor
Author
There was a problem hiding this comment.
I don't see the connection. I can't replace this lemma by an ofNat lemma since the statement depends on the parity.
3 tasks
callesonne
pushed a commit
that referenced
this pull request
May 16, 2024
Resplit `Algebra.BigOperators.List.Basic` and `Algebra.BigOperators.List.Lemmas` into two new files: * `Algebra.BigOperators.Group.List` for lemmas that require group-like structures (`Monoid`, `Group`, ...) * `Algebra.BigOperators.Ring.List` for lemmas that require ring-like structures (`MonoidWithZero`, `Ring`, ...) Add `assert_not_exists Ring` in the former. Once #11855 lands, it will be strenghtenable to `assert_not_exists MonoidWithZero`.
grunweg
pushed a commit
that referenced
this pull request
May 17, 2024
Resplit `Algebra.BigOperators.List.Basic` and `Algebra.BigOperators.List.Lemmas` into two new files: * `Algebra.BigOperators.Group.List` for lemmas that require group-like structures (`Monoid`, `Group`, ...) * `Algebra.BigOperators.Ring.List` for lemmas that require ring-like structures (`MonoidWithZero`, `Ring`, ...) Add `assert_not_exists Ring` in the former. Once #11855 lands, it will be strenghtenable to `assert_not_exists MonoidWithZero`.
|
You can run this locally as follows ## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
Algebra.GroupPower.BasicAlgebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 18, 2024
…ise` (#11855) The entire `Algebra.GroupPower` folder is problematic in that it treats `pow` as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of `pow` transversally. This PR scatters the lemmas in `Algebra.GroupPower.Basic` to earlier files and deletes it. Also delete `Algebra.GroupWithZero.Bitwise` whose lemmas are completely deprecated (and hard to rehome). See #9411 for previous work.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Algebra.GroupPower.Basic, Algebra.GroupWithZero.BitwiseAlgebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise
callesonne
pushed a commit
that referenced
this pull request
Jun 4, 2024
…ise` (#11855) The entire `Algebra.GroupPower` folder is problematic in that it treats `pow` as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of `pow` transversally. This PR scatters the lemmas in `Algebra.GroupPower.Basic` to earlier files and deletes it. Also delete `Algebra.GroupWithZero.Bitwise` whose lemmas are completely deprecated (and hard to rehome). See #9411 for previous work.
js2357
pushed a commit
that referenced
this pull request
Jun 18, 2024
…ise` (#11855) The entire `Algebra.GroupPower` folder is problematic in that it treats `pow` as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of `pow` transversally. This PR scatters the lemmas in `Algebra.GroupPower.Basic` to earlier files and deletes it. Also delete `Algebra.GroupWithZero.Bitwise` whose lemmas are completely deprecated (and hard to rehome). See #9411 for previous work.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 22, 2025
All lemmas in this file belong earlier. This finally gets rid of the `Algebra.GroupPower` folder, notorious for having caused imports increases in the algebra library (see #11855 for full motivation).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The entire
Algebra.GroupPowerfolder is problematic in that it treatspowas an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory ofpowtransversally.This PR scatters the lemmas in
Algebra.GroupPower.Basicto earlier files and deletes it. Also deleteAlgebra.GroupWithZero.Bitwisewhose lemmas are completely deprecated (and hard to rehome).See #9411 for previous work.