IsSepClosed

📁 Source: Mathlib/FieldTheory/IsSepClosed.lean

Statistics

Metric	Count
Definitions IsSepClosed, IsSepClosure, equiv	3
Theorems eq_bot_of_isSepClosed_of_isSeparable, algebraMap_surjective, degree_eq_one_of_irreducible, exists_aeval_eq_zero, exists_eq_mul_self, exists_eval₂_eq_zero, exists_eval₂_eq_zero_of_injective, exists_pow_nat_eq, exists_root, exists_root_C_mul_X_pow_add_C_mul_X_add_C, exists_root_C_mul_X_pow_add_C_mul_X_add_C', factors_of_separable, isAlgClosed_of_perfectField, lift_def, of_exists_root, of_isAlgClosed, roots_eq_zero_iff, splits_codomain, splits_domain, splits_of_separable, surjective_restrictDomain_of_isSeparable, isAlgClosure_of_perfectField, isAlgClosure_of_perfectField_top, isGalois, isSeparable, of_isAlgClosure_of_perfectField, self_of_isSepClosed, sep_closed, separable, isSepClosure_iff	30
Total	33

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_of_isSepClosed_of_isSeparable 📖	mathematical	—	Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	IsScalarTower.left bot_unique IsSepClosed.algebraMap_surjective SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass

IsSepClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_surjective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	minpoly.monic Algebra.IsSeparable.isIntegral Algebra.IsSeparable.isSeparable degree_eq_one_of_irreducible minpoly.irreducible instIsDomain minpoly.aeval add_eq_zero_iff_eq_neg Polynomial.aeval_C Polynomial.aeval_X Polynomial.aeval_add one_mul Polynomial.C_1 Polynomial.eq_X_add_C_of_degree_eq_one map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
degree_eq_one_of_irreducible 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable Semifield.toCommSemiring	Polynomial.degree WithBot WithBot.one Nat.instOne	—	Polynomial.Splits.degree_eq_one_of_irreducible splits_of_separable
exists_aeval_eq_zero 📖	mathematical	Polynomial.Separable	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	exists_eval₂_eq_zero_of_injective FaithfulSMul.algebraMap_injective
exists_eq_mul_self 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Nat.instAtLeastTwoHAddOfNat exists_pow_nat_eq sq
exists_eval₂_eq_zero 📖	mathematical	Polynomial.Separable CommRing.toCommSemiring	Polynomial.eval₂ CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	exists_eval₂_eq_zero_of_injective RingHom.injective IsLocalRing.toNontrivial Field.instIsLocalRing
exists_eval₂_eq_zero_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike Polynomial.Separable	Polynomial.eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	exists_root Polynomial.degree_map_eq_of_injective Polynomial.Separable.map Polynomial.eval₂_eq_eval_map Polynomial.IsRoot.eq_1
exists_pow_nat_eq 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Nat.cast_zero Polynomial.degree_X_pow_sub_C IsLocalRing.toNontrivial Field.instIsLocalRing LT.lt.ne' WithBot.coe_lt_coe pow_eq_zero_iff isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain exists_root Polynomial.separable_X_pow_sub_C Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_C
exists_root 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Polynomial.Splits.exists_eval_eq_zero splits_of_separable
exists_root_C_mul_X_pow_add_C_mul_X_add_C 📖	mathematical	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Polynomial.degree_ne_of_natDegree_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul zero_add Mathlib.Tactic.ComputeDegree.natDegree_eq_of_le_of_coeff_ne_zero' Polynomial.natDegree_add_le_of_le Polynomial.natDegree_mul_le_of_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.coeff_add_of_eq Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite Mathlib.Tactic.ComputeDegree.coeff_congr_lhs Polynomial.coeff_C Polynomial.coeff_X Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat le_refl mul_one add_zero Nat.cast_zero one_ne_zero Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Nat.cast_one le_trans one_le_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.natDegree_pow_le_of_le Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' one_pow sup_of_le_left Nat.instCanonicallyOrderedAdd Mathlib.Meta.NormNum.isNat_le_true Nat.instIsStrictOrderedRing LT.lt.ne' lt_of_lt_of_le zero_lt_two Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C Ne.isUnit exists_root Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_pow Polynomial.eval_X
exists_root_C_mul_X_pow_add_C_mul_X_add_C' 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	exists_root_C_mul_X_pow_add_C_mul_X_add_C CharP.cast_eq_zero_iff
factors_of_separable 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	splits_of_separable
isAlgClosed_of_perfectField 📖	mathematical	—	IsAlgClosed	—	IsAlgClosed.of_exists_root exists_root LT.lt.ne' Polynomial.degree_pos_of_irreducible PerfectField.separable_of_irreducible
lift_def 📖	mathematical	—	lift AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	—
of_exists_root 📖	mathematical	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	IsSepClosed	—	Polynomial.monic_mul_leadingCoeff_inv Irreducible.ne_zero Polynomial.irreducible_mul_leadingCoeff_inv Polynomial.Separable.mul_unit MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.instIsLocalHomRingHomC Polynomial.eval_mul Polynomial.eval_C IsDomain.to_noZeroDivisors instIsDomain Polynomial.uniqueFactorizationMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain UniqueFactorizationMonoid.factors_prod Polynomial.Splits.mul Polynomial.Splits.multisetProd UniqueFactorizationMonoid.irreducible_of_factor Polynomial.Separable.of_dvd UniqueFactorizationMonoid.dvd_of_mem_factors Polynomial.Splits.of_degree_eq_one Polynomial.degree_eq_one_of_irreducible_of_root IsUnit.splits Units.isUnit
of_isAlgClosed 📖	mathematical	—	IsSepClosed	—	IsAlgClosed.splits
roots_eq_zero_iff 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Multiset Multiset.instZero DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.coeff	—	instIsDomain le_or_gt Polynomial.eq_C_of_degree_le_zero exists_root LT.lt.ne' Polynomial.mem_roots Polynomial.ne_zero_of_degree_gt Polynomial.roots_C
splits_codomain 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.map	—	splits_of_separable Polynomial.Separable.map
splits_domain 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.map	—	Polynomial.Splits.map splits_of_separable
splits_of_separable 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	—
surjective_restrictDomain_of_isSeparable 📖	mathematical	—	AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommSemiring.toSemiring AlgHom.restrictDomain	—	IntermediateField.exists_algHom_of_splits' Algebra.IsSeparable.isIntegral splits_codomain Algebra.IsSeparable.isSeparable

IsSepClosure

Definitions

Name	Category	Theorems
equiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgClosure_of_perfectField 📖	mathematical	—	IsAlgClosure EuclideanDomain.toCommRing Field.toEuclideanDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring instIsDomain Field.toSemifield Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing separable instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors isAlgClosure_of_perfectField_top Algebra.IsAlgebraic.perfectField
isAlgClosure_of_perfectField_top 📖	mathematical	—	IsAlgClosure EuclideanDomain.toCommRing Field.toEuclideanDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring instIsDomain Field.toSemifield Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsSepClosed.isAlgClosed_of_perfectField sep_closed Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing separable
isGalois 📖	mathematical	—	IsGalois	—	separable Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing isSeparable IsSepClosed.splits_codomain sep_closed Algebra.IsSeparable.isSeparable
isSeparable 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	separable
of_isAlgClosure_of_perfectField 📖	mathematical	—	IsSepClosure	—	instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsSepClosed.of_isAlgClosed IsAlgClosure.isAlgClosed Algebra.IsAlgebraic.isSeparable_of_perfectField IsAlgClosure.isAlgebraic
self_of_isSepClosed 📖	mathematical	—	IsSepClosure Algebra.id Semifield.toCommSemiring Field.toSemifield	—	Algebra.isSeparable_self
sep_closed 📖	mathematical	—	IsSepClosed	—	—
separable 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	—

(root)

Definitions

Name	Category	Theorems
IsSepClosed 📖	CompData	8 math math: SeparableClosure.isSepClosed, isSepClosure_iff, IsSepClosed.of_isAlgClosed, Algebra.IsAlgebraic.isSepClosed, IsSepClosed.of_exists_root, isSepClosed_iff_isPurelyInseparable_algebraicClosure, IsSepClosed.separableClosure_eq_bot_iff, IsSepClosure.sep_closed
IsSepClosure 📖	CompData	4 math math: isSepClosure_iff, IsSepClosure.of_isAlgClosure_of_perfectField, separableClosure.isSepClosure, IsSepClosure.self_of_isSepClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSepClosure_iff 📖	mathematical	—	IsSepClosure IsSepClosed Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	IsSepClosure.sep_closed IsSepClosure.separable

---

← Back to Index