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(linear_algebra/invariant_submodule): invariant submodules #18289

Open
wants to merge 24 commits into
base: master
Choose a base branch
from
Open

feat(linear_algebra/invariant_submodule): invariant submodules #18289

wants to merge 24 commits into from

Conversation

themathqueen
Copy link
Collaborator

defining and proving some lemmas on invariant submodules

Open in Gitpod

@themathqueen themathqueen mentioned this pull request Jan 25, 2023
Open
2 tasks
@themathqueen themathqueen added awaiting-review The author would like community review of the PR undergrad Relates to undergrad.yaml t-algebra Algebra (groups, rings, fields etc) labels Jan 25, 2023
@themathqueen themathqueen mentioned this pull request Jan 25, 2023
Open
3 tasks
@themathqueen themathqueen added this to Done in linear_algebra Jan 25, 2023
alreadydone
alreadydone approved these changes Jan 26, 2023
View reviewed changes
src/linear_algebra/projection.lean Outdated Show resolved Hide resolved
src/linear_algebra/projection.lean Outdated Show resolved Hide resolved
src/linear_algebra/basic.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
@alreadydone
Copy link
Collaborator

Thanks!
maintainer merge

@github-actions
Copy link

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

@eric-wieser eric-wieser self-requested a review January 26, 2023 21:45
eric-wieser
eric-wieser reviewed Feb 2, 2023
View reviewed changes
src/linear_algebra/general_linear_group.lean Outdated Show resolved Hide resolved
src/linear_algebra/general_linear_group.lean Outdated Show resolved Hide resolved
src/linear_algebra/projection.lean Outdated Show resolved Hide resolved
src/linear_algebra/invariant_submodule.lean Outdated Show resolved Hide resolved
@themathqueen themathqueen removed the awaiting-review The author would like community review of the PR label Feb 3, 2023
@eric-wieser eric-wieser removed the undergrad Relates to undergrad.yaml label Feb 8, 2023
@eric-wieser eric-wieser added the awaiting-review The author would like community review of the PR label Feb 8, 2023
@semorrison semorrison added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 28, 2023
@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@semorrison
Copy link
Collaborator

I've created a zulip thread about this PR.

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

@alreadydone alreadydone alreadydone approved these changes

@ADedecker ADedecker ADedecker left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 t-algebra Algebra (groups, rings, fields etc)
Projects
linear_algebra
Review in progress
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@themathqueen @alreadydone @semorrison @eric-wieser @ADedecker