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

[Merged by Bors] - feat: port GroupTheory.FiniteAbelian #5730

Closed
wants to merge 38 commits into from
Closed

[Merged by Bors] - feat: port GroupTheory.FiniteAbelian #5730

wants to merge 38 commits into from

Conversation

mo271
Copy link
Collaborator

@mo271 mo271 commented Jul 5, 2023 •
edited by github-actions bot

Ruben-VandeVelde and others added 30 commits June 23, 2023 18:12
@Ruben-VandeVelde
feat: port Algebra.Module.Pid
aca460d
@Ruben-VandeVelde
Initial file copy from mathport
dd98d35
@Ruben-VandeVelde
automated fixes
54f2215 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Ruben-VandeVelde
Move
5462857
@Ruben-VandeVelde
Fix
6875708
@Ruben-VandeVelde
Fix
2ea7ed0
@Ruben-VandeVelde
Fix
17f30a5
@Ruben-VandeVelde
Fix
8b3aef6
@Ruben-VandeVelde
Small fix
400994b
@Ruben-VandeVelde
Small fix
b28ce13
@Ruben-VandeVelde
Small fix
b7a597c
@Ruben-VandeVelde
Small fix
d7f2240
@Ruben-VandeVelde
Small fix
953e82f
@Ruben-VandeVelde
Small fix
6ef3ae4
@Ruben-VandeVelde
Changes
0404143
@xroblot
Merge remote-tracking branch 'origin' into port/Algebra.Module.Pid
c33da60
@xroblot
Fix proof of torsion_by_prime_power_decomposition
4ac1183
@jcommelin
Merge remote-tracking branch 'origin/master' into port/Algebra.Module…
c773fba 
….Pid
@jcommelin
1 error left
5d25fdd
@mo271
lint
42ac1c9
@mo271
fix proof
6e07e7e
@mo271
unused var
b264775
@mo271
unused var 2
03ee194
@mo271
auto: naming
2c83a56
@mo271
manual: naming
43f9bee
@chabulhwi @mo271
style: remove unnecessary <| (#5721)
60ecd51
@kmill @mo271
chore: update Mathport/Syntax for #where command (#5718)
5f0d92c
@Komyyy @mo271
fix(Tactic.NormNum.LegendreSymbol): not a % 0 but a % 2 (#5719)
257caa0
@mo271
feat: port GroupTheory.FiniteAbelian
1a0f8bb
@mo271
Initial file copy from mathport
bc42ad8
mo271 added 3 commits July 5, 2023 13:01
@mo271
automated fixes
cb4474b 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@mo271
fix finite_of_fg_torsion
b329d7d
@mo271
progress in equiv_directSum_zMod_of_fintype
48dcd70
@mo271 mo271 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jul 5, 2023
@mo271
Copy link
Collaborator Author

mo271 commented Jul 5, 2023

Not sure if the instance Unique (Fin Nat.zero →₀ ℤ) should be added in some other place, but putting it right in the proof works. Should we add a porting note that this was inferred automatically before?

@mo271 mo271 added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jul 5, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR to Mathlib and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Jul 5, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 5, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 5, 2023
jcommelin
jcommelin approved these changes Jul 5, 2023
View reviewed changes
Copy link
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

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jul 5, 2023
bors bot pushed a commit that referenced this pull request Jul 5, 2023
@mo271 @jcommelin
@Ruben-VandeVelde @xroblot @chabulhwi @kmill @Komyyy
feat: port GroupTheory.FiniteAbelian (#5730)
f2c76a4 
- [x] depends on: #4707



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp>
@bors
Copy link

bors bot commented Jul 5, 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 feat: port GroupTheory.FiniteAbelian [Merged by Bors] - feat: port GroupTheory.FiniteAbelian Jul 5, 2023
@bors bors bot closed this Jul 5, 2023
@bors bors bot deleted the port/GroupTheory.FiniteAbelian branch July 5, 2023 18:51
semorrison pushed a commit that referenced this pull request Jul 6, 2023
@mo271 @jcommelin
@Ruben-VandeVelde @xroblot @chabulhwi @kmill @Komyyy @semorrison
feat: port GroupTheory.FiniteAbelian (#5730)
6f057c3 
- [x] depends on: #4707



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp>
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@mo271 @jcommelin
@Ruben-VandeVelde @xroblot @chabulhwi @kmill @Komyyy @kbuzzard
feat: port GroupTheory.FiniteAbelian (#5730)
84ecb98 
- [x] depends on: #4707



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp>
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@mo271 @jcommelin
@Ruben-VandeVelde @xroblot @chabulhwi @kmill @Komyyy @semorrison
feat: port GroupTheory.FiniteAbelian (#5730)
d66182f 
- [x] depends on: #4707



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp>
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
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
8 participants
@mo271 @semorrison @jcommelin @Ruben-VandeVelde @xroblot @chabulhwi @kmill @Komyyy