Jiang Jiedong

### Author Pages https://aclanthology.org/people/j/jiedong-jiang/ ### Type of Author Metadata Correction - [ ] The author page wrongly conflates different people with the same name. - [ ] This author has...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

feat(FieldTheory/Minpoly): `minpoly K x` splits implies `minpoly K (x + algebraMap K L a)` splits

5

We show that `minpoly K x` splits implies `minpoly K (x + algebraMap K L a)` splits. --- - [x] depends on: #17080 - [x] depends on: #17092 [![Open in...

feat(FieldTheory): add basic api's for relative algebraic closure

5

Move the definition of `algebraicClosure` into a separated file (mimicing `seperableClosure` in file FieldTheory.SeperableClosure). Add APIs for `algebraicClosure`. Most are copied api's from `separableClosure`. Show that every algebraic intermediate extension...

feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits

6

Add `minpoly K x` splits implies `minpoly K (- x)` splits and `minpoly K (algebraMap K L a - x)` splits. This is after #17093 . --- - [x] depends...

As suggested in the [PR review](https://github.com/leanprover-community/mathlib4/pull/17783#pullrequestreview-2394779847) of #17783, there is a task of refactoring theorem statements in field theory using `IsConjRoot`. Currently the definition of `IsConjRoot` is later than most...