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(LinearAlgebra/Matrix): center of special linear group #7826

Closed
wants to merge 54 commits into from
Closed

[Merged by Bors] - feat(LinearAlgebra/Matrix): center of special linear group #7826

wants to merge 54 commits into from

Conversation

shuxuezhuyi
Copy link
Collaborator

@shuxuezhuyi shuxuezhuyi commented Oct 21, 2023 •
edited

The center of a special linear group of degree n is a subgroup composed of scalar matrices,
in which the scalars are the n-th roots of 1.
Co-authored-by: Oliver Nash <github@olivernash.org>

Open in Gitpod

@shuxuezhuyi
feat(Data/Matrix): scalar if commutes with every stdBasisMatrix
8ff64e2
@shuxuezhuyi
name
f11cd7e
@shuxuezhuyi
feat(LinearAlgebra/Matrix): scalar if commutes with every nontrivial …
faf0805 
…transvection

`M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix).
@shuxuezhuyi
restate comm_all_stdBasisMatrix_nondiag
340af99
@shuxuezhuyi
Merge branch 'WenYang/comm_transvection_is_scalar' into WenYang/comm_…
9a12232 
…transvection_is_scalar2
@shuxuezhuyi
restate comm_all_TransvectionStruct
b69fe29
@shuxuezhuyi
feat(LinearAlgebra/Matrix): center of special linear group
6cdbc2c 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Oct 21, 2023
@shuxuezhuyi shuxuezhuyi added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Oct 21, 2023
@digama0
Copy link
Member

digama0 commented Oct 21, 2023

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

@shuxuezhuyi shuxuezhuyi mentioned this pull request Oct 22, 2023
Open
2 tasks
@ocfnash ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 18, 2024
@shuxuezhuyi @ocfnash
Apply suggestions from Oliver Nash
d0224c5 
Co-authored-by: Oliver Nash <github@olivernash.org>
@shuxuezhuyi shuxuezhuyi added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 19, 2024
@ocfnash
Copy link
Contributor

ocfnash commented Feb 19, 2024

Thanks for sticking with this; it looks good to me now. I won't send this to bors myself as I think I contributed a bit too heavily but I'll request someone else merge it.

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by ocfnash.

riccardobrasca
riccardobrasca approved these changes Feb 19, 2024
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca 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 d+

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 19, 2024

✌️ shuxuezhuyi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Feb 19, 2024
@shuxuezhuyi
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 19, 2024
@shuxuezhuyi @eric-wieser @digama0
feat(LinearAlgebra/Matrix): center of special linear group (#7826)
e478d1c 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
Co-authored-by: Oliver Nash <[github@olivernash.org](mailto:github@olivernash.org)>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LinearAlgebra/Matrix): center of special linear group [Merged by Bors] - feat(LinearAlgebra/Matrix): center of special linear group Feb 19, 2024
@mathlib-bors mathlib-bors bot closed this Feb 19, 2024
@mathlib-bors mathlib-bors bot deleted the WenYang/center_of_SL branch February 19, 2024 16:46
@mattrobball
Copy link
Collaborator

This should have been benchmarked. There are more new instructions in billions than new lines of code.

@riccardobrasca
Copy link
Member

This should have been benchmarked. There are more new instructions in billions than new lines of code.

Sorry for that, I didn't see any reason to do so. Do you have an idea of where the problem came from?

@mattrobball
Copy link
Collaborator

It looks like the ext i j in the Subsingleton instance takes 6+ seconds.

@mattrobball
Copy link
Collaborator

Correction the ext call in map_mul’ is the culprit

@mattrobball
Copy link
Collaborator

#10738 gets most of them back. I am not sure why things are so expanded at the start of this proof. More thought might yield better results than this

@ocfnash ocfnash mentioned this pull request Feb 20, 2024
Closed
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@shuxuezhuyi @eric-wieser
@digama0 @thorimur
feat(LinearAlgebra/Matrix): center of special linear group (#7826)
5c8d9e0 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
Co-authored-by: Oliver Nash <[github@olivernash.org](mailto:github@olivernash.org)>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
thorimur pushed a commit that referenced this pull request Feb 26, 2024
@shuxuezhuyi @eric-wieser
@digama0 @thorimur
feat(LinearAlgebra/Matrix): center of special linear group (#7826)
2b946f7 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
Co-authored-by: Oliver Nash <[github@olivernash.org](mailto:github@olivernash.org)>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@shuxuezhuyi @eric-wieser
@digama0 @riccardobrasca
feat(LinearAlgebra/Matrix): center of special linear group (#7826)
05aea7a 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
Co-authored-by: Oliver Nash <[github@olivernash.org](mailto:github@olivernash.org)>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@shuxuezhuyi @eric-wieser
@digama0 @dagurtomas
feat(LinearAlgebra/Matrix): center of special linear group (#7826)
38ddae1 
The center of a special linear group of degree `n` is a subgroup composed of scalar matrices,
in which the scalars are the `n`-th roots of `1`.
Co-authored-by: Oliver Nash <[github@olivernash.org](mailto:github@olivernash.org)>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ocfnash ocfnash ocfnash left review comments

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

@ocfnash ocfnash

Labels
delegated maintainer-merge t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@shuxuezhuyi @digama0 @leanprover-community-mathlib4-bot @ocfnash @mattrobball @riccardobrasca @eric-wieser