mathlib3
[Merged by Bors] - chore(field_theory/splitting_field): refactor `splitting_field`
#19178
Closed
Overview
Commits
67
Changes
View On GitHub

[Merged by Bors] - chore(field_theory/splitting_field): refactor `splitting_field` #19178

riccardobrasca wants to merge 67 commits into master from RB/splitting_field
riccardobrasca
riccardobrasca add instance
29f91f90
riccardobrasca riccardobrasca added WIP
github-actions github-actions added modifies-synchronized-file
eric-wieser
eric-wieser commented on 2023-06-12
eric-wieser
eric-wieser commented on 2023-06-12
riccardobrasca Update src/data/mv_polynomial/basic.lean
4cf39930
riccardobrasca let's start
ceccc246
eric-wieser refactor(field_theory/splitting_field/is_splitting_field): use `root_…
eb7e59cc
eric-wieser fix some downstream uses
f6c382e8
eric-wieser
eric-wieser fix
ea891339
eric-wieser fix
d5ff1791
eric-wieser fix
087d0119
eric-wieser golf
6d93f748
ericrbg fix
17779185
riccardobrasca term mode
e868d940
ericrbg fix
c55f3a87
ericrbg because I am silly
1fffef68
ericrbg golf
887ca9f8
riccardobrasca let's try this
24349da3
riccardobrasca Merge remote-tracking branch 'origin/eric-wieser/splitting_field-root…
efac9d47
ericrbg goodbye `decidable_eq`
6cdde619
riccardobrasca this looks good
44064859
riccardobrasca Merge remote-tracking branch 'origin/eric-wieser/splitting_field-root…
656d4dc1
riccardobrasca fix build
a46eed19
riccardobrasca
riccardobrasca commented on 2023-06-12
riccardobrasca long line
485eaefa
riccardobrasca fix this
2e39ec9f
riccardobrasca let's keep this
e9fc7061
ghost ghost added blocked-by-other-PR
riccardobrasca add missing instance
2c1ba52f
riccardobrasca add missing instances
28def5da
riccardobrasca surely better
d156a0f2
riccardobrasca let's try this
81abccac
riccardobrasca better
bc2ca428
riccardobrasca nicer
d91573f2
ghost ghost removed blocked-by-other-PR
riccardobrasca Merge remote-tracking branch 'origin/master' into RB/splitting_field
3d0d1357
riccardobrasca fix this
5e56143a
riccardobrasca lean needs help
a46c1664
riccardobrasca fix this
b4f69856
riccardobrasca not needed
4e9cac7e
riccardobrasca more help
99e0c6f6
riccardobrasca
riccardobrasca commented on 2023-06-12
riccardobrasca
riccardobrasca commented on 2023-06-12
riccardobrasca we need to fix this
9621efbe
riccardobrasca
riccardobrasca commented on 2023-06-13
riccardobrasca wow also this timeouts
203904bd
riccardobrasca fix the sorry
9a8ecd58
riccardobrasca fix this
da46c107
riccardobrasca let's see the rest of CI
ffd77fb6
riccardobrasca erase
517bcb4a
riccardobrasca Merge remote-tracking branch 'origin/master' into RB/splitting_field
f7eff3c8
riccardobrasca ops
06271de5
riccardobrasca riccardobrasca changed the title Backport !4#4891 chore(field_theory/splitting_field): refactor `splitting_field` 2 years ago
riccardobrasca lean needs help also here
86b141c0
riccardobrasca long line
123efae5
riccardobrasca test
d163d260
riccardobrasca Revert "test"
f5c285a8
riccardobrasca promising
99d39456
riccardobrasca maybe the last
9572c63e
riccardobrasca
riccardobrasca commented on 2023-06-13
riccardobrasca riccardobrasca removed WIP
riccardobrasca riccardobrasca added awaiting-review
riccardobrasca riccardobrasca added mathport
eric-wieser
eric-wieser commented on 2023-06-13
kim-em
kim-em commented on 2023-06-14
kim-em
kim-em commented on 2023-06-14
kim-em
kim-em commented on 2023-06-14
riccardobrasca remove comments and golf
bf90db7c
riccardobrasca one linter
911f638e
riccardobrasca riccardobrasca removed awaiting-review
riccardobrasca riccardobrasca added awaiting-author
riccardobrasca
riccardobrasca lint one file
55b676c2
riccardobrasca linter also for this file
a398e5ed
riccardobrasca linter and doc
e66ac9f5
riccardobrasca riccardobrasca removed awaiting-author
riccardobrasca riccardobrasca added awaiting-review
riccardobrasca riccardobrasca requested a review from ChrisHughes24 ChrisHughes24 2 years ago
riccardobrasca riccardobrasca requested a review from ericrbg ericrbg 2 years ago
riccardobrasca long line
50087f7a
riccardobrasca ops
058c63ce
eric-wieser
eric-wieser commented on 2023-06-14
ghost ghost added blocked-by-other-PR
riccardobrasca add porting comment
fdb82aa6
riccardobrasca linter
ff2b6e4c
riccardobrasca linter again
9eb58ce6
riccardobrasca typo
d51b6318
riccardobrasca typo again
7d715451
ghost ghost removed blocked-by-other-PR
riccardobrasca Merge remote-tracking branch 'origin/master' into RB/splitting_field
3264f495
eric-wieser
eric-wieser commented on 2023-06-14
riccardobrasca ops
867fde5c
riccardobrasca ops again
bfcc3433
riccardobrasca riccardobrasca removed modifies-synchronized-file
ghost
ericrbg
riccardobrasca useless
91bf7f0a
riccardobrasca Revert "useless"
37d66543
riccardobrasca useless
6404534d
riccardobrasca
jcommelin
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title chore(field_theory/splitting_field): refactor `splitting_field` [Merged by Bors] - chore(field_theory/splitting_field): refactor `splitting_field` 2 years ago
bors bors closed this 2 years ago
bors bors deleted the RB/splitting_field branch 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge mathport
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum