is_splitting_field): use `root_set`
#19179

Closed

[Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set` #19179

eric-wieser wants to merge 11 commits into master from eric-wieser/splitting_field-rootset

refactor(field_theory/splitting_field/is_splitting_field): use `root_…

eb7e59cc

eric-wieser added awaiting-review

eric-wieser added awaiting-CI

eric-wieser marked this pull request as ready for review 2 years ago

github-actions added modifies-synchronized-file

fix some downstream uses

f6c382e8

fix

ea891339

fix

d5ff1791

fix

087d0119

golf

6d93f748

fix

17779185

fix

c55f3a87

eric-wieser commented on 2023-06-12

because I am silly

1fffef68

eric-wieser added mathport

golf

887ca9f8

goodbye `decidable_eq`

6cdde619

github-actions removed awaiting-CI

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~refactor(field_theory/splitting_field/is_splitting_field): use `root_set`~~ [Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set` 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/splitting_field-rootset branch 2 years ago

Reviewers

ericrbg

Assignees

No one assigned

Labels

ready-to-merge mathport modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set` #19179 Closed

[Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set` #19179

mathlib3
[Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set`
#19179

Closed