Structures · Algebra
IsAlgClosure
Typeclass for an extension being an algebraic closure.
- Defined in
- Mathlib.FieldTheory.IsAlgClosed.Basic
- Shape
- 2 explicit arguments · adds isAlgClosed, isAlgebraic
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 by20
- IsAlgClosure.equivOfEquiv
- IsAlgClosure.isAlgClosed
- IsAlgClosure.equivOfAlgebraic'
- IsAlgClosure.equivOfEquiv_algebraMap
- IsAlgClosure.equiv
- isSepClosed_iff_isPurelyInseparable_algebraicClosure
- IsAlgClosure.equivOfEquivAux
- IsAlgClosure.equivOfEquiv_comp_algebraMap
- IsAlgClosure.equivOfEquiv_symm_algebraMap
- IsAlgClosure.isAlgebraic
- IsAlgClosure.ofAlgebraic
- IsAlgClosure.normal
- IsAlgClosure.isGalois
- IsAlgClosure.separable
- IsAlgClosure.equivOfAlgebraic
- IsSepClosure.of_isAlgClosure_of_perfectField
- IsAlgClosure.equivOfEquiv.congr_simp
- IsAlgClosure.equivOfEquiv_symm_comp_algebraMap
- perfectField_iff_isSeparable_algebraicClosure
- IsAlgClosure.equivOfAlgebraic'.congr_simp
Ancestors0
No ancestors.