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.
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.
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
feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits #17369
base: master
Are you sure you want to change the base?
feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits #17369
Changes from 1 commit
d0ed84a
41a78df
3bed6d4
18041da
f0e9e6e
5523b69
0d02fe2
0f3e600
836e4c0
7a2eb0b
668ffdb
ecca48e
98e9329
1cfa845
0fbf224
7367e35
0778212
5d7d0ba
4f49cb9
842354b
fb6e9ca
f5c04bf
9642033
fdc3d39
bc86def
2bb6c58
99198a1
864a8d3
3358e8a
780408c
e79f878
7696960
5ca101c
7607c22
0b7ef8b
a1e2788
8dfd2ac
55d0693
3304b55
0de5911
1236b66
aa7ccba
c8a5f98
b1d42fd
e90afad
b7b85a3
4dd7f6f
82ee24d
5506205
11bec1f
b0a970c
27151b0
0fb14cd
8dc6273
e5b8d0b
1b41103
1d155a0
4c7ca1e
ef443e5
4b334fc
bc146ca
be5a312
b5d4a09
701b866
57b9c47
f784583
8ff2d2b
f8edc7f
e170f81
be93423
9fb3ea5
04a1b1a
ec58248
761e8dc
62ff556
fdb1aca
d1b5777
75c09e2
c570985
ae0b95a
2c3e355
8ce7810
5714d2e
90871b9
5fbcf89
fc1202a
ad2bf7d
dfa10e0
095b1e4
2d5cfc4
0a11ad0
1fcd038
0f04fc2
30c6e23
fca365a
7b945dc
cc02c3f
a4b04bb
c7404a1
f936545
3e1c6ea
63b013b
9539e9e
7972465
6ffe1e2
8bd924a
f58eed6
71512b5
30fcf13
c2efc9d
48edd5d
2ffb4a9
e3a4868
baae113
3d5f2df
cfd0e0b
a012e24
7702c28
1bc31fc
05da8ac
93b1b5c
9259a73
c586548
6a8f1b1
745e29b
6ef40ff
f72a0fe
73f95ea
fc5d246
d76a894
47950c2
95dd466
3efc7d2
a31c511
f9f16d6
b8e4cab
cd0c264
738d3f7
77ee86d
ca952ba
afbe019
22f28f7
3aa40e9
46c338d
7afc5f6
f7e9705
19324c0
a212515
86c9625
138e391
db22294
db987c9
9218c6f
31f3081
c91a635
1c2e5e3
c8691ec
fdb4bbf
09b6dae
6836c03
01b02b3
350d9e4
858ac88
8dcb1af
19f24f9
31b44f5
e961c33
357587c
66fff9d
7b37861
5303e11
b40d246
741889d
9ba135d
3316bf0
72065b9
0bf8038
eb15858
a20dbd5
0f0321a
8a1888f
c7a0959
eb7844c
f38a9b6
969a007
74ef1a7
158f0ea
c4bc187
a8b0b51
20903ba
db74127
47e9ef7
5a3697c
81a7c48
864d7cc
120c9de
0174355
c2fc55f
8315d6b
1b75741
124104e
cc619b3
1fc9157
cefeaa1
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
Check failure on line 574 in Mathlib/Algebra/Polynomial/AlgebraMap.lean
GitHub Actions / Lint style
Check failure on line 574 in Mathlib/Algebra/Polynomial/AlgebraMap.lean
GitHub Actions / Lint style