Structures · Algebra
IsSepClosed
Typeclass for separably closed fields.
To show Polynomial.Splits p f for an arbitrary ring homomorphism f,
see IsSepClosed.splits_codomain and IsSepClosed.splits_domain.
- Defined in
- Mathlib.FieldTheory.IsSepClosed
- Shape
- One type argument · adds splits_of_separable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- SeparableClosure
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- AlgebraicGeometry.Scheme.pointSmallEtale
- AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage
- IsSepClosed.exists_root
- IsSepClosed.splits_of_separable
- IsSepClosed.lift
- CommAlgCat.FiniteEtale.equivOfIsSepClosed
- Algebra.FormallyEtale.equivPiOfIsSepClosed
- IsSepClosed.exists_aeval_eq_zero
- IsSepClosed.algebraMap_surjective
- IsSepClosed.exists_eval₂_eq_zero_of_injective
- IsSepClosed.degree_eq_one_of_irreducible
- AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective
- IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C
- IsSepClosed.surjective_domRestrict_of_isSeparable
- IsSepClosed.algebraMap_bijective
- AlgebraicGeometry.Scheme.isConservative_pointSmallEtale
- IntermediateField.eq_bot_of_isSepClosed_of_isSeparable
- AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe
- IsSepClosed.exists_pow_nat_eq
- AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed
- IsSepClosed.splits_codomain
- IsSepClosed.separableClosure_eq_bot_iff
- IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed
- Algebra.FormallyEtale.equivPiOfIsSepClosed_comap
- AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage.congr_simp
- AlgebraicGeometry.Scheme.pointSmallEtale.congr_simp
- IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C'
- IsSepClosed.roots_eq_zero_iff
- Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed
- IsSepClosedOfCharZero.isCyclotomicExtension
- IsSepClosed.surjective_restrictDomain_of_isSeparable
- WeierstrassCurve.exists_variableChange_of_j_eq
- AlgebraicGeometry.Scheme.pointSmallEtale_fiber
- CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiberOfIsSepClosed
- CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_map
- CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiniteSpecOfIsSepClosed
- CommAlgCat.FiniteEtale.fiberIsoFiniteSpec
- CommAlgCat.FiniteEtale.fiberIsoComp
- IsSepClosed.isCyclotomicExtension
- Algebra.IsFiniteSplit.instOfIsSepClosedOfEssFiniteTypeOfFormallyEtale
- IsSepClosure.self_of_isSepClosed
- IsSepClosed.hasEnoughRootsOfUnity
- IsSepClosed.exists_eq_mul_self
- separableClosure.isSepClosure
- AlgebraicGeometry.Scheme.geometricFiber
- IsSepClosed.exists_eval₂_eq_zero
- Algebra.IsAlgebraic.isSepClosed
- IsSepClosed.splits_domain
- CommAlgCat.FiniteEtale.equivOfIsSepClosed_inverse_obj
- Algebra.FormallyEtale.equivPiOfIsSepClosed_self_apply
Ancestors0
No ancestors.