mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open jjdishere opened this issue 1 year ago • 5 comments
trafficstars

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 is contained in the algebraic closure.

  • [x] depends on: #14206

Open in Gitpod

jjdishere avatar Sep 13 '24 15:09 jjdishere