mathlib3
feat(linear_algebra/invariant_submodule): invariant submodules
#18289

Open

feat(linear_algebra/invariant_submodule): invariant submodules #18289

themathqueen wants to merge 24 commits into master from invariant_submodule

feat(linear_algebra/invariant_submodule): invariant submodules

a7cd215b

themathqueen added awaiting-review

themathqueen added undergrad

themathqueen added t-algebra

themathqueen requested a review from

ADedecker 2 years ago

themathqueen requested a review from

eric-wieser 2 years ago

ADedecker commented on 2023-01-25

eric-wieser commented on 2023-01-25

fix after review

76f89f85

eric-wieser commented on 2023-01-25

fix after review

8dfae616

eric-wieser commented on 2023-01-25

fix after review

7da94bd7

alreadydone commented on 2023-01-25

fix

6e296808

alreadydone commented on 2023-01-26

alreadydone approved these changes on 2023-01-26

fixed stuff, changed names and added docstrings

1cf0de66

moved lemma to la/basic

0454ea31

eric-wieser requested a review from

eric-wieser 2 years ago

eric-wieser commented on 2023-01-26

ADedecker commented on 2023-01-27

changes after review

67de946f

add todo

3e0d8012

themathqueen requested a review from

eric-wieser 2 years ago

eric-wieser commented on 2023-01-30

fixes after review

dc4437ce

eric-wieser commented on 2023-02-01

merge branch

4172305b

fix merge

459d90b1

themathqueen requested a review from

eric-wieser 2 years ago

eric-wieser commented on 2023-02-02

changes after review

8ea48f4c

changed name

39168b45

added lemma

accaa222

themathqueen removed awaiting-review

eric-wieser commented on 2023-02-03

change name

62867498

themathqueen requested a review from

eric-wieser 2 years ago

eric-wieser removed undergrad

eric-wieser commented on 2023-02-08

eric-wieser added awaiting-review

changes after review

a2404387

eric-wieser commented on 2023-02-08

remove lemma

19b5ba93

kim-em requested a review from

eric-wieser 2 years ago

kim-em added modifies-synchronized-file

eric-wieser added not-too-late

eric-wieser commented on 2023-07-25

Update src/linear_algebra/general_linear_group.lean

cb42b2a1

add the general form of the lemmas

7307edad

cleanup

427c883a

missing backtick

f591c22e

correct lemma name

10b09f20

golf, remove a questionable set lemma

591b14e4

Reviewers

alreadydone

eric-wieser

ADedecker

Assignees

No one assigned

Labels

awaiting-review t-algebra modifies-synchronized-file not-too-late

Milestone

No milestone

mathlib3 feat(linear_algebra/invariant_submodule): invariant submodules #18289 Open

feat(linear_algebra/invariant_submodule): invariant submodules #18289

mathlib3
feat(linear_algebra/invariant_submodule): invariant submodules
#18289

Open