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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 CommRing.toCommSemiring 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₂ 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_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.toPow 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 Field.toSemifield	—	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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	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' instReflLe 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.toPow 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 Field.toSemifield	—	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 Field.toSemifield 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 Field.toSemifield Polynomial.map	—	splits_of_separable Polynomial.Separable.map
splits_domain 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map	—	Polynomial.Splits.map splits_of_separable
splits_of_separable 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
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