Structures · Algebra
IsNormalClosure
L/F is a normal closure of K/F if the minimal polynomial of every element of K over F
splits in L, and L is generated by roots of such minimal polynomials over F.
(Since the minimal polynomial of a transcendental element is 0,
the normal closure of K/F is the same as the normal closure over F
of the algebraic closure of F in K.)
- Defined in
- Mathlib.FieldTheory.Normal.Closure
- Shape
- 3 explicit arguments · adds splits, adjoin_rootSet
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by5
Ancestors0
No ancestors.