Theorems · Inductive type · field theory
IsSepClosed
(k : Type u) → [Field k] → Prop
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
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement · cited by 7,404
Cited by53
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.pointSmallEtalestatement and proof · cited by 7
- IsSepClosed.exists_rootstatement and proof · cited by 4
- IsSepClosed.splits_of_separablestatement and proof · cited by 4
- AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimagestatement and proof · cited by 4
- IsSepClosed.liftstatement · cited by 3
- Algebra.FormallyEtale.equivPiOfIsSepClosedstatement and proof · cited by 3
- CommAlgCat.FiniteEtale.equivOfIsSepClosedstatement and proof · cited by 3
- IsSepClosed.algebraMap_surjectivestatement and proof · cited by 2
- IsSepClosed.exists_aeval_eq_zerostatement and proof · cited by 2
- IsSepClosed.exists_eval₂_eq_zero_of_injectivestatement and proof · cited by 2
- isSepClosed_iff_isPurelyInseparable_algebraicClosurestatement and proof · cited by 1
- IsSepClosed.algebraMap_bijectivestatement and proof · cited by 1