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 CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly	Fintype.card AlgHom CommRing.toCommSemiring PowerBasis.AlgHom.fintype 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 CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly	Nat.card AlgHom CommRing.toCommSemiring PowerBasis.dim	—	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	59 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, 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, 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	—	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 📖	—	Associated Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable	—	—	Polynomial.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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Polynomial.derivative_one Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
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	—	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 📖	—	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike IsSeparable	—	—	isSeparable_map_iff
of_algHom 📖	—	IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	—	—	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	DFunLike.coe	—	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	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	EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Polynomial.Separable.of_dvd Polynomial.Separable.map minpoly.dvd_map_of_isScalarTower

Polynomial

Definitions

Name	Category	Theorems
Separable 📖	MathDef	37 math math: separable_X_add_C, separable_X_pow_sub_C_unit, PerfectField.separable_of_irreducible, ConjRootClass.separable_minpoly, separable_X_pow_sub_C_of_irreducible, separable_X_pow_sub_C, nodup_aroots_iff_of_splits, separable_or, X_pow_sub_C_separable_iff, card_rootSet_eq_natDegree_iff_of_splits, not_separable_zero, Associated.separable_iff, separable_X, separable_C_mul_X_pow_add_C_mul_X_add_C', separable_X_pow_sub_C', natSepDegree_eq_natDegree_iff, IsGalois.is_separable_splitting_field, separable_def', separable_one, IsPrimitiveRoot.separable_minpoly_mod, separable_prod_X_sub_C_iff', separable_prod_X_sub_C_iff, X_pow_sub_one_separable_iff, separable_C, separable_def, Irreducible.separable, PerfectField.separable_iff_squarefree, separable_iff_derivative_ne_zero, exists_separable_of_irreducible, separable_of_subsingleton, nodup_roots_iff_of_splits, separable_cyclotomic, IsGalois.tfae, separable_C_mul_X_pow_add_C_mul_X_add_C, separable_X_sub_C, 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.toNatPow 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.toNatPow 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 CommSemiring.toSemiring algebraMap	Fintype.card Set.Elem rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain rootSetFintype natDegree	—	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 CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	Fintype.card Set.Elem rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain rootSetFintype natDegree Separable	—	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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat emultiplicity AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	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 instMul semiring 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	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	Separable Semifield.toCommSemiring DFunLike.coe AlgHom CommSemiring.toSemiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow 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 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.toNatPow Nat.instMonoid	IsUnit DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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 CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	Multiset.Nodup aroots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Separable	—	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 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 IsOrderedRing.toZeroLEOneClass 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 Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow 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 Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow 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.toNatPow 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.toNatPow 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 Polynomial instSub Monoid.toNatPow 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	EuclideanDomain.gcd Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instEuclideanDomain	—	Separable.of_dvd EuclideanDomain.gcd_dvd_left
separable_gcd_right 📖	mathematical	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	—	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 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	Finset.prod CommRing.toCommMonoid commRing Finset.univ	—	separable_prod'
separable_prod' 📖	mathematical	IsCoprime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring Separable	Finset.prod 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.toNatPow 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 Finset.instMembership	—	—	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	—	IsCoprime.of_mul_left_left IsCoprime.of_mul_right_right IsCoprime.of_add_mul_left_right Polynomial.derivative_mul
map 📖	mathematical	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.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.instMul	—	Associated.separable associated_mul_unit_right
ne_zero 📖	—	Polynomial.Separable	—	—	Polynomial.not_separable_zero
of_dvd 📖	—	Polynomial.Separable Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring	—	—	of_mul_left
of_mul_left 📖	—	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	—	—	IsCoprime.of_mul_left_left IsCoprime.of_mul_right_left IsCoprime.of_add_mul_left_right Polynomial.derivative_mul
of_mul_right 📖	—	Polynomial.Separable Polynomial CommSemiring.toSemiring Polynomial.instMul	—	—	of_mul_left mul_comm
of_pow 📖	—	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.Separable Monoid.toNatPow	—	—	of_pow'
of_pow' 📖	mathematical	Polynomial.Separable Polynomial CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	IsUnit	—	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.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	20 math math: IntermediateField.isSeparable_of_mem_isSeparable, isSeparable_map_iff, Algebra.IsSeparable.isSeparable, Field.isSeparable_algebraMap, AlgEquiv.isSeparable_iff, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', IsSeparable.of_integral, isSeparable_algebraMap, IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, Subalgebra.isSeparable_iff, Algebra.isSeparable_iff, Algebra.isSeparable_def, IntermediateField.isSeparable_adjoin_simple_iff_isSeparable, Algebra.IsSeparable.isSeparable', JacobsonNoether.exists_separable_and_not_isCentral', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, mem_separableClosure_iff, IsGalois.separable, JacobsonNoether.exists_separable_and_not_isCentral, 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 map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_X Polynomial.aeval_C sub_self
isSeparable_map_iff 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	IsSeparable	—	minpoly.algHom_eq

---

← Back to Index