Structures · Algebra
PerfectField
A perfect field.
See also PerfectRing for a generalisation in positive characteristic.
- Defined in
- Mathlib.FieldTheory.Perfect
- Shape
- One type argument · adds separable_of_irreducible
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- PerfectClosure
- Ideal.ResidueField
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
- LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg
- Ideal.ramificationIdx_eq_one_iff
- Module.End.IsSemisimple.of_mem_adjoin_pair
- Module.End.exists_isNilpotent_isSemisimple
- PerfectField.separable_of_irreducible
- Module.End.IsSemisimple.sub_of_commute
- Ideal.card_inertia_eq_ramificationIdxIn
- Algebra.IsAlgebraic.perfectField
- Ideal.card_stabilizer_eq
- Ideal.card_stabilizer_eq_card_inertia_mul_finrank
- PerfectField.separable_iff_squarefree
- Ideal.absNorm_relNorm
- Ideal.ncard_primesOver_mul_card_inertia_mul_finrank
- LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'
- Ideal.relNorm_eq_pow_of_isMaximal
- AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField
- LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra
- Ideal.ramificationIdx'_eq_one_iff
- LieAlgebra.ad_isSemisimple_of_isSemisimple
- Module.End.isNilpotent_isSemisimple_unique
- LieAlgebra.ad_mem_adjoin_of_isSemisimple
- perfectField_of_perfectClosure_eq_bot
- perfectField_of_isSeparable_of_perfectField_top
- PerfectField.toPerfectRing
- Ring.instFiniteNormalClosure_1
- PerfectField.of_ringEquiv
- Ring.instFiniteNormalClosure
- IsPurelyInseparable.bijective_comp_algebraMap
- LieAlgebra.ad_mem_adjoin_of_isNilpotent
- IsSepClosure.isAlgClosure_of_perfectField
- Algebra.FormallySmooth.of_perfectField
- exists_isTranscendenceBasis_and_isSeparable_of_perfectField
- IsSepClosure.of_isAlgClosure_of_perfectField
- IsSepClosure.isAlgClosure_of_perfectField_top
- PerfectField.splits_of_natSepDegree_eq_one
- Module.End.IsSemisimple.add_of_commute
- Ring.instIsGaloisFractionRingNormalClosure
- Module.End.IsSemisimple.mul_of_commute
- Ring.instIsDedekindDomainNormalClosure
- Ring.HasFiniteQuotients.instPerfectFieldResidueFieldOfFractionRing
- perfectClosure.perfectField
- IsPurelyInseparable.bijective_restrictDomain
- IsPurelyInseparable.instNonemptyAlgHomOfPerfectField
- IsSepClosed.isAlgClosed_of_perfectField
- Algebra.IsAlgebraic.isSeparable_of_perfectField
- AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField
- Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
Ancestors0
No ancestors.