Separable

📁 Source: Mathlib/FieldTheory/Separable.lean

Statistics

Metric	Count
Definitions IsSeparable, IsSeparable, Separable	3
Theorems isSeparable, isSeparable_iff, isSeparable_iff, card_of_powerBasis, natCard_of_powerBasis, isAlgebraic, isIntegral, isSeparable, isSeparable', of_algHom, of_equiv_equiv, of_integral, isSeparable_def, isSeparable_iff, isSeparable_self, isSeparable_tower_bot_of_isSeparable, isSeparable_tower_top_of_isSeparable, separable, separable_iff, isSeparable_tower_bot, isSeparable_tower_top, separable, isIntegral, map, of_algHom, of_equiv_equiv, of_integral, tower_bot, tower_top, aeval_derivative_ne_zero, eval₂_derivative_ne_zero, inj_of_prod_X_sub_C, injective_of_prod_X_sub_C, isCoprime, map, mul, mul_unit, ne_zero, of_dvd, of_mul_left, of_mul_right, of_pow, of_pow', squarefree, unit_mul, X_pow_sub_C_separable_iff, X_pow_sub_one_separable_iff, card_rootSet_eq_natDegree, card_rootSet_eq_natDegree_iff_of_splits, count_roots_le_one, emultiplicity_le_one_of_separable, eq_X_sub_C_of_separable_of_root_eq, exists_finset_of_splits, exists_separable_of_irreducible, isUnit_of_self_mul_dvd_separable, isUnit_or_eq_zero_of_separable_expand, nodup_aroots_iff_of_splits, nodup_of_separable_prod, nodup_roots, nodup_roots_iff_of_splits, not_separable_zero, rootMultiplicity_le_one_of_separable, separable_C, separable_C_mul_X_pow_add_C_mul_X_add_C, separable_C_mul_X_pow_add_C_mul_X_add_C', separable_X, separable_X_add_C, separable_X_pow_sub_C, separable_X_pow_sub_C', separable_X_pow_sub_C_unit, separable_X_sub_C, separable_def, separable_def', separable_gcd_left, separable_gcd_right, separable_iff_derivative_ne_zero, separable_map, separable_of_subsingleton, separable_one, separable_or, separable_prod, separable_prod', separable_prod_X_sub_C_iff, separable_prod_X_sub_C_iff', unique_separable_of_irreducible, isSeparable_iff, isSeparable_algebraMap, isSeparable_map_iff	88
Total	91

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_iff 📖	mathematical	—	IsSeparable DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring instFunLike	—	minpoly.algEquiv_eq

AlgEquiv.Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable 📖	mathematical	—	Algebra.IsSeparable	—	AlgEquiv.isSeparable_iff Algebra.IsSeparable.isSeparable
isSeparable_iff 📖	mathematical	—	Algebra.IsSeparable	—	isSeparable

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_of_powerBasis 📖	mathematical	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing PowerBasis.gen Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map algebraMap Semifield.toCommSemiring minpoly	Fintype.card AlgHom Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring PowerBasis.AlgHom.fintype CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain PowerBasis.dim	—	instIsDomain Fintype.card_eq_nat_card natCard_of_powerBasis
natCard_of_powerBasis 📖	mathematical	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing PowerBasis.gen Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map algebraMap Semifield.toCommSemiring minpoly	Nat.card AlgHom Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring PowerBasis.dim EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing	—	instIsDomain Nat.card_congr Nat.subtype_card Multiset.mem_toFinset PowerBasis.natDegree_minpoly IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.natDegree_map DivisionRing.isSimpleRing Polynomial.Splits.natDegree_eq_card_roots Multiset.toFinset_card_of_nodup Polynomial.nodup_roots Polynomial.separable_map

Algebra

Definitions

Name	Category	Theorems
IsSeparable 📖	CompData	61 math math: instIsSeparableResidueFieldOfFormallyUnramified, IsSeparable.of_equiv_equiv, FixedPoints.isSeparable, traceForm_nondegenerate_tfae, isSepClosure_iff, instIsSeparableQuotientIdealOfResidueField, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, FormallyUnramified.iff_map_maximalIdeal_eq, FractionRing.isSeparable_of_isLocalization, FormallyUnramified.iff_isSeparable, instIsSeparableResidueFieldOfQuotientIdeal, Subalgebra.isSeparable_iff, FormallyEtale.iff_isSeparable, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, le_separableClosure_iff, IsSepClosure.isSeparable, eq_separableClosure_iff, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, separableClosure.eq_top_iff, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, isSeparable_tower_top_of_isSeparable, isUnramifiedAt_iff_map_eq, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, WithAbs.instIsSeparable_1, isSeparable_iff, isSeparable_def, instIsSeparableResidueFieldOfIsUnramifiedAt, IntermediateField.isSeparable_adjoin_simple_iff_isSeparable, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top, FormallyUnramified.isSeparable, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, isGalois_iff, isSeparable_tower_bot_of_isSeparable, IntermediateField.isSeparable_tower_bot, IsAlgClosure.separable, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, perfectField_iff_isSeparable_algebraicClosure, FormallyEtale.iff_exists_algEquiv_prod, AlgEquiv.Algebra.isSeparable_iff, IntermediateField.isSeparable_adjoin_pair_of_isSeparable, IntermediateField.isSeparable_sup, IntermediateField.isSeparable_iSup, isSeparable_self, separableClosure.isSeparable, Field.finSepDegree_eq_finrank_iff, isSeparable_iff_finInsepDegree_eq_one, AlgEquiv.Algebra.isSeparable, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, IsSeparable.of_algHom, isSeparable_residueField_iff, WithAbs.instIsSeparable, Etale.iff_exists_algEquiv_prod, IsSepClosure.separable, IsGalois.to_isSeparable, IntermediateField.isSeparable_tower_top, IsSeparable.trans, IsAlgebraic.isSeparable_of_perfectField, IsCyclotomicExtension.isSeparable, IsSeparable.of_integral, IntermediateField.isSeparable_adjoin_iff_isSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_def 📖	mathematical	—	IsSeparable IsSeparable	—	—
isSeparable_iff 📖	mathematical	—	IsSeparable IsIntegral IsSeparable	—	IsSeparable.isIntegral IsSeparable.isSeparable
isSeparable_self 📖	mathematical	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing id CommRing.toCommSemiring	—	isSeparable_algebraMap
isSeparable_tower_bot_of_isSeparable 📖	mathematical	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	IsSeparable.tower_bot IsSeparable.isSeparable
isSeparable_tower_top_of_isSeparable 📖	mathematical	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsSeparable.tower_top IsSeparable.isSeparable

Algebra.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic 📖	mathematical	—	Algebra.IsAlgebraic	—	IsIntegral.isAlgebraic isIntegral
isIntegral 📖	mathematical	—	IsIntegral	—	IsSeparable.isIntegral isSeparable
isSeparable 📖	mathematical	—	IsSeparable	—	isSeparable'
isSeparable' 📖	mathematical	—	IsSeparable	—	—
of_algHom 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	IsSeparable.of_algHom isSeparable
of_equiv_equiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsSeparable.of_equiv_equiv isSeparable RingEquiv.apply_symm_apply
of_integral 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsSeparable.of_integral

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separable 📖	mathematical	Associated Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable	Polynomial.Separable	—	—
separable_iff 📖	mathematical	Associated Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Separable	—	separable symm

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_tower_bot 📖	mathematical	—	Algebra.IsSeparable IntermediateField SetLike.instMembership instSetLike EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing toField algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	Algebra.isSeparable_tower_bot_of_isSeparable IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing isScalarTower_mid'
isSeparable_tower_top 📖	mathematical	—	Algebra.IsSeparable IntermediateField SetLike.instMembership instSetLike EuclideanDomain.toCommRing Field.toEuclideanDomain toField DivisionRing.toRing Field.toDivisionRing instAlgebraSubtypeMem Ring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield	—	Algebra.isSeparable_tower_top_of_isSeparable IsScalarTower.left isScalarTower_mid'

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separable 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield	—	Polynomial.separable_iff_derivative_ne_zero Polynomial.degree_eq_bot Polynomial.degree_derivative_eq IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain natDegree_pos

IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	IsSeparable	IsIntegral	—	subsingleton_or_nontrivial Polynomial.monic_one Module.subsingleton of_not_not Polynomial.Separable.ne_zero minpoly.eq_zero
map 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike IsSeparable	IsSeparable DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	—	isSeparable_map_iff
of_algHom 📖	mathematical	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	tower_bot IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.of_algebraMap_eq AlgHom.commutes
of_equiv_equiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSeparable	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Algebra.commutes RingEquiv.map_mul' RingEquiv.map_add' RingEquiv.apply_symm_apply DFunLike.congr_fun AlgEquiv.isSeparable_iff tower_top IsScalarTower.of_algebraMap_eq RingHom.congr_arg RingEquiv.symm_apply_apply
of_integral 📖	mathematical	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Irreducible.separable minpoly.irreducible instIsDomain Algebra.IsIntegral.isIntegral
tower_bot 📖	mathematical	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring RingHom.instFunLike algebraMap	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	minpoly.dvd Polynomial.aeval_algebraMap_eq_zero_iff instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors minpoly.aeval Polynomial.Separable.of_mul_left
tower_top 📖	mathematical	IsSeparable	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Polynomial.Separable.of_dvd Polynomial.Separable.map minpoly.dvd_map_of_isScalarTower

Polynomial

Definitions

Name	Category	Theorems
Separable 📖	MathDef	51 math math: separable_X_add_C, separable_X_pow_sub_C_unit, PerfectField.separable_of_irreducible, ConjRootClass.separable_minpoly, Associated.separable, separable_X_pow_sub_C_of_irreducible, separable_X_pow_sub_C, nodup_aroots_iff_of_splits, separable_or, Separable.unit_mul, Separable.mul_unit, X_pow_sub_C_separable_iff, card_rootSet_eq_natDegree_iff_of_splits, not_separable_zero, Associated.separable_iff, separable_X, Separable.of_mul_left, separable_C_mul_X_pow_add_C_mul_X_add_C', separable_X_pow_sub_C', separable_prod, natSepDegree_eq_natDegree_iff, IsGalois.is_separable_splitting_field, separable_def', separable_one, IsPrimitiveRoot.separable_minpoly_mod, separable_prod_X_sub_C_iff', Separable.of_pow', separable_prod_X_sub_C_iff, X_pow_sub_one_separable_iff, Separable.map, separable_C, separable_def, separable_gcd_right, separable_gcd_left, Irreducible.separable, PerfectField.separable_iff_squarefree, separable_iff_derivative_ne_zero, exists_separable_of_irreducible, separable_of_subsingleton, nodup_roots_iff_of_splits, separable_prod', separable_cyclotomic, Separable.of_mul_right, IsGalois.tfae, separable_C_mul_X_pow_add_C_mul_X_add_C, separable_X_sub_C, Separable.of_dvd, Separable.of_pow, Separable.mul, separable_map, galois_poly_separable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_pow_sub_C_separable_iff 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	not_isUnit_of_natDegree_pos IsDomain.to_noZeroDivisors instIsDomain natDegree_sub_C natDegree_pow natDegree_X IsLocalRing.toNontrivial Field.instIsLocalRing mul_one derivative_sub derivative_X_pow map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul derivative_C sub_self separable_X_pow_sub_C
X_pow_sub_one_separable_iff 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X instOne	—	pow_zero sub_self IsLocalRing.toNontrivial Field.instIsLocalRing Nat.cast_zero X_pow_sub_C_separable_iff one_ne_zero NeZero.one
card_rootSet_eq_natDegree 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring map algebraMap	Fintype.card Set.Elem rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield rootSetFintype natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	instIsDomain Fintype.card_congr' rootSet_def Fintype.card_coe Multiset.toFinset_card_of_nodup nodup_roots Separable.map Splits.natDegree_eq_card_roots natDegree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing
card_rootSet_eq_natDegree_iff_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map algebraMap Semifield.toCommSemiring	Fintype.card Set.Elem rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield rootSetFintype natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Separable Semifield.toCommSemiring	—	instIsDomain Fintype.card_congr' rootSet_def Fintype.card_coe natDegree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Splits.natDegree_eq_card_roots nodup_aroots_iff_of_splits
count_roots_le_one 📖	mathematical	Separable CommRing.toCommSemiring	Multiset.count roots	—	count_roots rootMultiplicity_le_one_of_separable IsDomain.toNontrivial
emultiplicity_le_one_of_separable 📖	mathematical	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Separable	ENat instLEENat emultiplicity Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Mathlib.Tactic.Contrapose.contrapose₂ isUnit_of_self_mul_dvd_separable sq pow_dvd_of_le_emultiplicity Order.add_one_le_of_lt
eq_X_sub_C_of_separable_of_root_eq 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Splits map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff instSub DivisionRing.toRing Field.toDivisionRing X	—	instIsDomain not_separable_zero IsLocalRing.toNontrivial Field.instIsLocalRing nodup_roots Separable.map Finset.nodup Finset.eq_singleton_iff_unique_mem mem_roots map_ne_zero DivisionRing.isSimpleRing IsRoot.def eval₂_eq_eval_map eval₂_hom map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_injective RingHom.injective map_mul map_C map_sub map_X leadingCoeff_map Splits.eq_X_sub_C_of_single_root
exists_finset_of_splits 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring map	Finset map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Finset.prod CommRing.toCommMonoid commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instSub DivisionRing.toRing Field.toDivisionRing X	—	splits_iff_exists_multiset Finset.prod_eq_multiset_prod nodup_of_separable_prod IsLocalRing.toNontrivial Field.instIsLocalRing Separable.of_mul_right Separable.map Multiset.toFinset_eq leadingCoeff_map DivisionRing.isSimpleRing
exists_separable_of_irreducible 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Separable Semifield.toCommSemiring DFunLike.coe AlgHom CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toPow Nat.instMonoid	—	CharP.char_is_prime_or_zero IsDomain.to_noZeroDivisors instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing Nat.strong_induction_on separable_or pow_zero expand_one Irreducible.ne_zero C_0 isUnit_iff_ne_zero separable_C degree_le_zero_iff natDegree_eq_zero_iff_degree_le_zero natDegree_expand MulZeroClass.zero_mul mul_one Nat.Prime.one_lt Ne.bot_lt expand_expand pow_succ'
isUnit_of_self_mul_dvd_separable 📖	mathematical	Separable Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring instMul	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	isCoprime_self mul_add Distrib.leftDistribClass derivative_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one IsCoprime.of_mul_right_left IsCoprime.of_mul_left_left
isUnit_or_eq_zero_of_separable_expand 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toPow Nat.instMonoid	IsUnit Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	derivative_expand Nat.cast_pow CharP.cast_eq_zero instCharP zero_pow MulZeroClass.zero_mul MulZeroClass.mul_zero isUnit_iff IsDomain.to_noZeroDivisors instIsDomain isCoprime_zero_right separable_def expand_eq_C pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass isUnit_C
nodup_aroots_iff_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map algebraMap Semifield.toCommSemiring	Multiset.Nodup aroots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Separable Semifield.toCommSemiring	—	instIsDomain nodup_roots_iff_of_splits map_ne_zero DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing separable_map
nodup_of_separable_prod 📖	mathematical	Separable CommRing.toCommSemiring Multiset.prod Polynomial CommSemiring.toSemiring CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	Multiset.Nodup	—	Multiset.nodup_iff_ne_cons_cons not_isUnit_X_sub_C isUnit_of_self_mul_dvd_separable Multiset.map_cons Multiset.prod_cons mul_dvd_mul_left dvd_mul_right
nodup_roots 📖	mathematical	Separable CommRing.toCommSemiring	Multiset.Nodup roots	—	Multiset.nodup_iff_count_le_one count_roots_le_one
nodup_roots_iff_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Multiset.Nodup roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Separable Semifield.toCommSemiring	—	instIsDomain Function.mtr Splits.exists_eval_eq_zero Splits.of_dvd GCDMonoid.gcd_dvd_left isUnit_iff_degree_eq_zero gcd_isUnit_iff IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd Separable.eq_1 LT.lt.trans_eq one_lt_rootMultiplicity_iff_isRoot_gcd count_roots nodup_roots
not_separable_zero 📖	mathematical	—	Separable Polynomial CommSemiring.toSemiring instZero	—	MulZeroClass.mul_zero derivative_zero add_zero NeZero.one nontrivial
rootMultiplicity_le_one_of_separable 📖	mathematical	Separable CommRing.toCommSemiring	rootMultiplicity CommRing.toRing	—	rootMultiplicity_zero Nat.instCanonicallyOrderedAdd rootMultiplicity_eq_multiplicity Nat.cast_le IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Nat.cast_one FiniteMultiplicity.emultiplicity_eq_multiplicity finiteMultiplicity_X_sub_C emultiplicity_le_one_of_separable not_isUnit_X_sub_C
separable_C 📖	mathematical	—	Separable DFunLike.coe RingHom Polynomial CommSemiring.toSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	separable_def derivative_C isCoprime_zero_right isUnit_C
separable_C_mul_X_pow_add_C_mul_X_add_C 📖	mathematical	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	IsUnit.exists_left_inv map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass derivative_mul derivative_C MulZeroClass.zero_mul derivative_X_pow map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.mul_zero add_zero derivative_X mul_one zero_add right_distrib Distrib.rightDistribClass add_assoc neg_mul mul_comm neg_add_cancel map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
separable_C_mul_X_pow_add_C_mul_X_add_C' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	separable_C_mul_X_pow_add_C_mul_X_add_C CharP.cast_eq_zero_iff
separable_X 📖	mathematical	—	Separable X CommSemiring.toSemiring	—	separable_def derivative_X isCoprime_one_right
separable_X_add_C 📖	mathematical	—	Separable Polynomial CommSemiring.toSemiring instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	separable_def derivative_add derivative_X derivative_C add_zero isCoprime_one_right
separable_X_pow_sub_C 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommSemiring.toSemiring instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	separable_X_pow_sub_C_unit
separable_X_pow_sub_C' 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommSemiring.toSemiring instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	separable_X_pow_sub_C CharP.cast_eq_zero_iff
separable_X_pow_sub_C_unit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instSub CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Units.val	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nat.cast_zero NeZero.one separable_def' IsUnit.exists_left_inv derivative_sub derivative_C sub_zero derivative_pow derivative_X mul_one RingHom.map_mul C_eq_natCast Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Units.inv_mul RingHom.map_one sub_add_cancel
separable_X_sub_C 📖	mathematical	—	Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	sub_eq_add_neg C_neg separable_X_add_C
separable_def 📖	mathematical	—	Separable IsCoprime Polynomial CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	—
separable_def' 📖	mathematical	—	Separable Polynomial CommSemiring.toSemiring instAdd instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative instOne	—	—
separable_gcd_left 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield	Separable Semifield.toCommSemiring Field.toSemifield EuclideanDomain.gcd Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instEuclideanDomain	—	Separable.of_dvd EuclideanDomain.gcd_dvd_left
separable_gcd_right 📖	mathematical	Separable Semifield.toCommSemiring Field.toSemifield	Separable Semifield.toCommSemiring Field.toSemifield EuclideanDomain.gcd Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instEuclideanDomain	—	Separable.of_dvd EuclideanDomain.gcd_dvd_right
separable_iff_derivative_ne_zero 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Separable Semifield.toCommSemiring Field.toSemifield	—	Irreducible.not_isUnit isCoprime_zero_right EuclideanDomain.isCoprime_of_dvd Irreducible.isUnit_or_isUnit Units.mul_right_dvd not_lt_of_ge natDegree_le_of_dvd IsDomain.to_noZeroDivisors instIsDomain natDegree_derivative_lt derivative_of_natDegree_zero
separable_map 📖	mathematical	—	Separable CommRing.toCommSemiring map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring Semifield.toCommSemiring	—	Ideal.exists_maximal Ideal.instIsTwoSided_1 Separable.map isCoprime_map derivative_map separable_def map_map
separable_of_subsingleton 📖	mathematical	—	Separable	—	Unique.instSubsingleton
separable_one 📖	mathematical	—	Separable Polynomial CommSemiring.toSemiring instOne	—	isCoprime_one_left
separable_or 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Separable Semifield.toCommSemiring Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe AlgHom CommSemiring.toSemiring algebraOfAlgebra Algebra.id AlgHom.funLike expand	—	natDegree_eq_zero_of_derivative_eq_zero IsAddTorsionFree.of_isCancelMulZero_charZero CharP.charP_to_charZero IsDomain.toIsCancelMulZero instIsDomain LT.lt.ne' natDegree_pos_iff_degree_pos degree_pos_of_irreducible separable_iff_derivative_ne_zero Irreducible.of_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass isLocalHom_expand expand_contract IsDomain.to_noZeroDivisors
separable_prod 📖	mathematical	Pairwise Function.onFun Polynomial CommSemiring.toSemiring CommRing.toCommSemiring IsCoprime commSemiring Separable	Separable CommRing.toCommSemiring Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommMonoid commRing Finset.univ	—	separable_prod'
separable_prod' 📖	mathematical	IsCoprime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring Separable	Separable CommRing.toCommSemiring Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommMonoid commRing	—	Finset.induction_on separable_one Finset.prod_insert Separable.mul IsCoprime.prod_right
separable_prod_X_sub_C_iff 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Finset.prod Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommMonoid commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.univ instSub DivisionRing.toRing Field.toDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	separable_prod_X_sub_C_iff'
separable_prod_X_sub_C_iff' 📖	mathematical	—	Separable Semifield.toCommSemiring Field.toSemifield Finset.prod Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommMonoid commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instSub DivisionRing.toRing Field.toDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Separable.inj_of_prod_X_sub_C IsLocalRing.toNontrivial Field.instIsLocalRing Finset.prod_attach separable_prod' pairwise_coprime_X_sub_C separable_X_sub_C
unique_separable_of_irreducible 📖	—	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Separable Semifield.toCommSemiring DFunLike.coe AlgHom CommSemiring.toSemiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toPow Nat.instMonoid	—	—	le_iff_exists_add Nat.instCanonicallyOrderedAdd isUnit_or_eq_zero_of_separable_expand isUnit_iff IsDomain.to_noZeroDivisors instIsDomain isUnit_C Irreducible.not_isUnit expand_C add_zero pow_zero expand_one pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass expand_mul pow_add le_of_not_ge

Polynomial.Separable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_derivative_ne_zero 📖	—	Polynomial.Separable DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	eval₂_derivative_ne_zero
eval₂_derivative_ne_zero 📖	—	Polynomial.Separable Polynomial.eval₂ CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	Polynomial.eval₂_add Polynomial.eval₂_mul MulZeroClass.mul_zero add_zero Polynomial.eval₂_one NeZero.one
inj_of_prod_X_sub_C 📖	—	Polynomial.Separable CommRing.toCommSemiring Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommMonoid Polynomial.commRing Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Finset SetLike.instMembership Finset.instSetLike	—	—	of_pow Polynomial.not_isUnit_X_sub_C two_ne_zero of_mul_left sq mul_assoc Finset.prod_insert Finset.notMem_erase Finset.insert_erase Finset.mem_erase_of_ne_of_mem
injective_of_prod_X_sub_C 📖	—	Polynomial.Separable CommRing.toCommSemiring Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	—	inj_of_prod_X_sub_C Finset.mem_univ
isCoprime 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	IsCoprime Polynomial CommSemiring.toSemiring Polynomial.commSemiring	—	IsCoprime.of_mul_left_left IsCoprime.of_mul_right_right IsCoprime.of_add_mul_left_right Polynomial.derivative_mul
map 📖	mathematical	Polynomial.Separable	Polynomial.Separable Polynomial.map CommSemiring.toSemiring	—	Polynomial.derivative_map Polynomial.map_mul Polynomial.map_add Polynomial.map_one
mul 📖	mathematical	Polynomial.Separable CommRing.toCommSemiring IsCoprime Polynomial CommSemiring.toSemiring Polynomial.commSemiring	Polynomial.Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring Polynomial.instMul	—	Polynomial.separable_def Polynomial.derivative_mul IsCoprime.mul_left IsCoprime.add_mul_left_right IsCoprime.mul_right IsCoprime.mul_add_right_right IsCoprime.symm
mul_unit 📖	mathematical	Polynomial.Separable IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	—	Associated.separable associated_mul_unit_right
ne_zero 📖	—	Polynomial.Separable	—	—	Polynomial.not_separable_zero
of_dvd 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring	Polynomial.Separable	—	of_mul_left
of_mul_left 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	Polynomial.Separable	—	IsCoprime.of_mul_left_left IsCoprime.of_mul_right_left IsCoprime.of_add_mul_left_right Polynomial.derivative_mul
of_mul_right 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	Polynomial.Separable	—	of_mul_left mul_comm
of_pow 📖	mathematical	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable Monoid.toPow	Polynomial.Separable	—	of_pow'
of_pow' 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable	—	pow_one isCoprime_self IsCoprime.of_mul_left_right isCoprime pow_succ
squarefree 📖	mathematical	Polynomial.Separable	Squarefree Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	squarefree_iff_emultiplicity_le_one Polynomial.emultiplicity_le_one_of_separable
unit_mul 📖	mathematical	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	—	Associated.separable associated_unit_mul_right

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_iff 📖	mathematical	—	Algebra.IsSeparable Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership instSetLike toRing algebra IsSeparable	—	isSeparable_map_iff Subtype.val_injective

(root)

Definitions

Name	Category	Theorems
IsSeparable 📖	MathDef	31 math math: IntermediateField.isSeparable_of_mem_isSeparable, IsSeparable.map, isSeparable_map_iff, Algebra.IsSeparable.isSeparable, IsSeparable.of_algebra_isSeparable_of_isSeparable, Field.isSeparable_algebraMap, AlgEquiv.isSeparable_iff, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', IsSeparable.of_integral, isSeparable_algebraMap, Field.isSeparable_neg, IsSeparable.of_algHom, IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, Field.isSeparable_mul, Subalgebra.isSeparable_iff, Field.isSeparable_add, Field.isSeparable_inv, Algebra.isSeparable_iff, Algebra.isSeparable_def, IntermediateField.isSeparable_adjoin_simple_iff_isSeparable, IsSeparable.tower_bot, Algebra.IsSeparable.isSeparable', IsSeparable.tower_top, Field.isSeparable_sub, JacobsonNoether.exists_separable_and_not_isCentral', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, mem_separableClosure_iff, IsGalois.separable, JacobsonNoether.exists_separable_and_not_isCentral, IsSeparable.of_equiv_equiv, IntermediateField.isSeparable_adjoin_iff_isSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_algebraMap 📖	mathematical	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring RingHom.instFunLike algebraMap	—	Polynomial.Separable.of_dvd Polynomial.separable_X_sub_C minpoly.dvd Polynomial.aeval_sub Polynomial.aeval_X Polynomial.aeval_C sub_self
isSeparable_map_iff 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	IsSeparable DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	—	minpoly.algHom_eq

---

← Back to Index