-
Notifications
You must be signed in to change notification settings - Fork 297
[Merged by Bors] - feat(field_theory/algebraic_closure): algebraic closure #3733
Conversation
This comment has been minimized.
This comment has been minimized.
Delighted to see this. I was literally just looking for the definition of algebraically closed fields three days ago, when writing this. Looking forward to updating one this merges. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking forward to merging this PR. The structure looks good, I left some comments on the documentation. I didn't have time to look closely at style.
@@ -321,6 +321,8 @@ begin | |||
... ≤ v (a + s) : aux (a + s) (-s) (by rwa ←ideal.neg_mem_iff at h) | |||
end | |||
|
|||
local attribute [-instance] classical.DLO |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you add a comment (linking to Zulip?) explaining why this instance is problematic here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
- `is_alg_closure k K` is the typeclass saying `K` is an algebraic closure of `k`. | ||
|
||
- `algebraic_closure k` is an algebraic closure of `k` (in the same universe). | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you add a description of the construction you are using, and a bibliography reference if you followed a book or paper? There are many ways to prove this theorem and it would help to know which one you use.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Style / indentation comments.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Thanks! bors r+ |
👎 Rejected by label |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors r+
```lean instance : is_alg_closed (algebraic_closure k) := ``` TODO: Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma). Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Pull request successfully merged into master. Build succeeded: |
instance : is_alg_closed (algebraic_closure k) :=
TODO: Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma).