SeparableDegree

📁 Source: Mathlib/FieldTheory/SeparableDegree.lean

Statistics

Metric	Count
Definitions `Emb`, `embEquivOfAdjoinSplits`, `embEquivOfEquiv`, `embEquivOfIsAlgClosed`, `embProdEmbOfIsAlgebraic`, `finSepDegree`, `instInhabitedEmb`, `natSepDegree`	8
Theorems `trans`, `finSepDegree_eq`, `finSepDegree_dvd_finrank`, `finSepDegree_eq_finrank_iff`, `finSepDegree_eq_finrank_of_isSeparable`, `finSepDegree_eq_of_adjoin_splits`, `finSepDegree_eq_of_equiv`, `finSepDegree_eq_of_isAlgClosed`, `finSepDegree_eq_zero_of_transcendental`, `finSepDegree_le_finrank`, `finSepDegree_mul_finSepDegree_of_isAlgebraic`, `finSepDegree_self`, `infinite_emb_of_transcendental`, `instNeZeroFinSepDegree`, `isSeparable_add`, `isSeparable_algebraMap`, `isSeparable_inv`, `isSeparable_mul`, `isSeparable_neg`, `isSeparable_sub`, `finSepDegree_adjoin_simple_eq_finrank_iff`, `finSepDegree_adjoin_simple_eq_natSepDegree`, `finSepDegree_adjoin_simple_le_finrank`, `finSepDegree_bot`, `finSepDegree_bot'`, `finSepDegree_top`, `isSeparable_adjoin_pair_of_isSeparable`, `isSeparable_adjoin_simple_iff_isSeparable`, `isSeparable_of_mem_isSeparable`, `natSepDegree_dvd_natDegree`, `natSepDegree_eq_one_iff_of_monic`, `natSepDegree_eq_one_iff_of_monic'`, `of_algebra_isSeparable_of_isSeparable`, `splits_of_natSepDegree_eq_one`, `natSepDegree_eq`, `natSepDegree_eq`, `eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible`, `eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one`, `eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits`, `natSepDegree_eq_one_iff`, `natSepDegree_eq_one_iff_of_irreducible`, `natSepDegree_eq_one_iff_of_irreducible'`, `natSepDegree_eq_natDegree`, `natSepDegree_C`, `natSepDegree_C_mul`, `natSepDegree_C_mul_X_sub_C_pow`, `natSepDegree_X`, `natSepDegree_X_pow`, `natSepDegree_X_pow_char_pow_sub_C`, `natSepDegree_X_sub_C`, `natSepDegree_X_sub_C_pow`, `natSepDegree_eq_natDegree_iff`, `natSepDegree_eq_natDegree_of_separable`, `natSepDegree_eq_of_isAlgClosed`, `natSepDegree_eq_of_splits`, `natSepDegree_eq_zero`, `natSepDegree_eq_zero_iff`, `natSepDegree_expand`, `natSepDegree_le_natDegree`, `natSepDegree_le_of_dvd`, `natSepDegree_map`, `natSepDegree_mul`, `natSepDegree_mul_eq_iff`, `natSepDegree_mul_of_isCoprime`, `natSepDegree_ne_zero`, `natSepDegree_ne_zero_iff`, `natSepDegree_one`, `natSepDegree_pow`, `natSepDegree_pow_of_ne_zero`, `natSepDegree_smul_nonzero`, `natSepDegree_zero`, `natSepDegree_eq_one_iff_eq_X_pow_sub_C`, `natSepDegree_eq_one_iff_eq_X_sub_C_pow`, `natSepDegree_eq_one_iff_eq_expand_X_sub_C`, `natSepDegree_eq_one_iff_pow_mem`, `perfectField_iff_splits_of_natSepDegree_eq_one`	76
Total	84

Algebra.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans` 📖	mathematical	—	`Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsSeparable.of_algebra_isSeparable_of_isSeparable` `isSeparable`

Field

Definitions

Name	Category	Theorems
`Emb` 📖	CompOp	9 math math: `Emb.Cardinal.two_le_deg`, `Emb.Cardinal.succEquiv_coherence`, `Emb.cardinal_eq`, `Emb.cardinal_eq_of_isSeparable`, `Emb.Cardinal.deg_lt_aleph0`, `Emb.cardinal_eq_two_pow_sepDegree`, `infinite_emb_of_transcendental`, `Emb.cardinal_eq_two_pow_rank`, `Emb.cardinal_separableClosure`
`embEquivOfAdjoinSplits` 📖	CompOp	—
`embEquivOfEquiv` 📖	CompOp	—
`embEquivOfIsAlgClosed` 📖	CompOp	—
`embProdEmbOfIsAlgebraic` 📖	CompOp	—
`finSepDegree` 📖	CompOp	22 math math: `finSepDegree_eq_of_isAlgClosed`, `finSepDegree_mul_finInsepDegree`, `finSepDegree_eq_of_equiv`, `finSepDegree_self`, `IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff`, `finSepDegree_le_finrank`, `finSepDegree_eq_finrank_of_isSeparable`, `IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree`, `IntermediateField.finSepDegree_adjoin_simple_le_finrank`, `finSepDegree_mul_finSepDegree_of_isAlgebraic`, `Algebra.IsSeparable.finSepDegree_eq`, `instNeZeroFinSepDegree`, `isPurelyInseparable_iff_finSepDegree_eq_one`, `finSepDegree_dvd_finrank`, `finSepDegree_eq`, `finSepDegree_eq_zero_of_transcendental`, `IntermediateField.finSepDegree_bot'`, `finSepDegree_eq_finrank_iff`, `IntermediateField.finSepDegree_top`, `finSepDegree_eq_of_adjoin_splits`, `IsPurelyInseparable.finSepDegree_eq_one`, `IntermediateField.finSepDegree_bot`
`instInhabitedEmb` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finSepDegree_dvd_finrank` 📖	mathematical	—	`finSepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `IntermediateField.finSepDegree_top` `finrank_top` `IntermediateField.induction_on_adjoin` `IntermediateField.finSepDegree_bot` `IntermediateField.finrank_bot` `IntermediateField.isScalarTower_mid'` `mul_dvd_mul` `Module.finrank_mul_finrank` `IntermediateField.instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `instIsLocalRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.isAlgebraic_tower_bot` `IntermediateField.isAlgebraic_tower_top` `Algebra.IsAlgebraic.of_finite` `Module.finrank_of_infinite_dimensional` `dvd_zero`
`finSepDegree_eq_finrank_iff` 📖	mathematical	—	`finSepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Algebra.IsSeparable` `DivisionRing.toRing` `toDivisionRing`	—	`IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `instIsLocalRing` `IsScalarTower.left` `IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff` `le_antisymm` `IntermediateField.finSepDegree_adjoin_simple_le_finrank` `le_of_not_gt` `finSepDegree_le_finrank` `IntermediateField.finiteDimensional_right` `instNeZeroFinSepDegree` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `neg_eq_zero` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.isAlgebraic_tower_top` `Algebra.IsAlgebraic.of_finite` `finSepDegree_eq_finrank_of_isSeparable`
`finSepDegree_eq_finrank_of_isSeparable` 📖	mathematical	—	`finSepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `IntermediateField.finSepDegree_top` `finrank_top` `IntermediateField.induction_on_adjoin` `IntermediateField.finSepDegree_bot` `IntermediateField.finrank_bot` `IntermediateField.isScalarTower_mid'` `IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff` `IsAlgebraic.of_finite` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `instIsLocalRing` `IntermediateField.finiteDimensional_right` `IsSeparable.tower_top` `Algebra.IsSeparable.isSeparable` `Module.finrank_mul_finrank` `IntermediateField.instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `commRing_strongRankCondition` `Module.Free.of_divisionRing` `finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.isAlgebraic_tower_bot` `IntermediateField.isAlgebraic_tower_top` `Algebra.IsSeparable.isAlgebraic` `Module.finrank_of_infinite_dimensional` `IntermediateField.exists_lt_finrank_of_infinite_dimensional` `IntermediateField.isSeparable_tower_bot` `MulZeroClass.mul_zero` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_zero` `Mathlib.Tactic.Ring.mul_congr` `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.zero_mul` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `sub_eq_zero_of_eq` `Nat.cast_mul`
`finSepDegree_eq_of_adjoin_splits` 📖	mathematical	`IntermediateField.adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsIntegral` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly`	`finSepDegree` `Nat.card` `AlgHom`	—	`Nat.card_congr`
`finSepDegree_eq_of_equiv` 📖	mathematical	—	`finSepDegree`	—	`Nat.card_congr`
`finSepDegree_eq_of_isAlgClosed` 📖	mathematical	—	`finSepDegree` `Nat.card` `AlgHom` `Semifield.toCommSemiring` `toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Nat.card_congr`
`finSepDegree_eq_zero_of_transcendental` 📖	mathematical	—	`finSepDegree`	—	`Nat.card_eq_zero_of_infinite` `infinite_emb_of_transcendental`
`finSepDegree_le_finrank` 📖	mathematical	—	`finSepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `instIsLocalRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `finSepDegree_dvd_finrank`
`finSepDegree_mul_finSepDegree_of_isAlgebraic` 📖	mathematical	—	`finSepDegree`	—	`Nat.card_prod` `Nat.card_congr`
`finSepDegree_self` 📖	mathematical	—	`finSepDegree` `Algebra.id` `Semifield.toCommSemiring` `toSemifield`	—	`finSepDegree.eq_1` `Nat.card_eq_one_iff_unique` `AlgHom.subsingleton` `Unique.instSubsingleton`
`infinite_emb_of_transcendental` 📖	mathematical	—	`Infinite` `Emb`	—	`exists_isTranscendenceBasis'` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `instIsLocalRing` `IsTranscendenceBasis.isAlgebraic_field` `IsScalarTower.left` `Equiv.infinite_iff` `IntermediateField.isScalarTower_mid'` `Prod.infinite_of_left` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `IsTranscendenceBasis.nonempty_iff_transcendental` `AlgebraicClosure.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsScalarTower.coe_toAlgHom'` `IsScalarTower.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `MvPolynomial.nontrivial_of_nontrivial` `MvPolynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsFractionRing.injective` `Localization.isLocalization` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `MvPolynomial.algebraicIndependent_polynomial_aeval_X` `Transcendental.pow` `Polynomial.transcendental_X` `Infinite.of_injective` `instInfiniteNat` `IsFractionRing.lift_algebraMap` `MvPolynomial.bind₁_X_right` `MvPolynomial.totalDegree_X_pow`
`instNeZeroFinSepDegree` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `finSepDegree`	—	`Nat.card_ne_zero` `Fintype.finite` `instIsDomain`
`isSeparable_add` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IntermediateField.isSeparable_of_mem_isSeparable` `IntermediateField.isSeparable_adjoin_pair_of_isSeparable` `IntermediateField.add_mem` `IntermediateField.subset_adjoin`
`isSeparable_algebraMap` 📖	mathematical	—	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `toSemifield` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`isSeparable_algebraMap`
`isSeparable_inv` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `toSemifield`	—	`IntermediateField.isSeparable_of_mem_isSeparable` `IsScalarTower.left` `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable` `IntermediateField.inv_mem` `IntermediateField.mem_adjoin_simple_self`
`isSeparable_mul` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IntermediateField.isSeparable_of_mem_isSeparable` `IntermediateField.isSeparable_adjoin_pair_of_isSeparable` `IntermediateField.mul_mem` `IntermediateField.subset_adjoin`
`isSeparable_neg` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`IntermediateField.isSeparable_of_mem_isSeparable` `IsScalarTower.left` `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable` `IntermediateField.neg_mem` `IntermediateField.mem_adjoin_simple_self`
`isSeparable_sub` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`IntermediateField.isSeparable_of_mem_isSeparable` `IntermediateField.isSeparable_adjoin_pair_of_isSeparable` `IntermediateField.sub_mem` `IntermediateField.subset_adjoin`

Field.Algebra.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finSepDegree_eq` 📖	mathematical	—	`Field.finSepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Field.finSepDegree_eq_finrank_of_isSeparable`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finSepDegree_adjoin_simple_eq_finrank_iff` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `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` `Module.finrank` `module'` `IsSeparable`	—	`IsScalarTower.left` `finSepDegree_adjoin_simple_eq_natSepDegree` `adjoin.finrank` `IsAlgebraic.isIntegral` `Polynomial.natSepDegree_eq_natDegree_iff` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsSeparable.eq_1`
`finSepDegree_adjoin_simple_eq_natSepDegree` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `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` `Polynomial.natSepDegree` `minpoly`	—	`IsScalarTower.left` `instIsDomain` `Nat.card_congr` `IsAlgebraic.isIntegral` `Nat.card_eq_fintype_card` `Polynomial.natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `Fintype.card_coe` `Fintype.card_congr'`
`finSepDegree_adjoin_simple_le_finrank` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `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` `Module.finrank` `module'`	—	`IsScalarTower.left` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `adjoin.finiteDimensional` `IsAlgebraic.isIntegral` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`finSepDegree_bot` 📖	mathematical	—	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `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` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `Field.finSepDegree_eq_of_equiv` `Field.finSepDegree_self`
`finSepDegree_bot'` 📖	mathematical	—	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.finSepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower` `IsScalarTower.right`
`finSepDegree_top` 📖	mathematical	—	`Field.finSepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.finSepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower`
`isSeparable_adjoin_pair_of_isSeparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `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`	—	`IsScalarTower.left` `isScalarTower_mid'` `adjoin_simple_adjoin_simple` `IsSeparable.tower_top` `Algebra.IsSeparable.trans` `instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `isSeparable_adjoin_simple_iff_isSeparable`
`isSeparable_adjoin_simple_iff_isSeparable` 📖	mathematical	—	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `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` `IsSeparable`	—	`IsScalarTower.left` `isSeparable_of_mem_isSeparable` `mem_adjoin_simple_self` `IsSeparable.isIntegral` `Field.finSepDegree_eq_finrank_iff` `adjoin.finiteDimensional` `finSepDegree_adjoin_simple_eq_finrank_iff` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isSeparable_of_mem_isSeparable` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `instSetLike`	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsScalarTower.left` `minpoly_eq` `Algebra.IsSeparable.isSeparable`

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_dvd_natDegree` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.natSepDegree` `Polynomial.natDegree`	—	`ExpChar.exists` `instIsDomain` `hasSeparableContraction` `Polynomial.HasSeparableContraction.natSepDegree_eq` `Polynomial.HasSeparableContraction.dvd_degree`
`natSepDegree_eq_one_iff_of_monic` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.natSepDegree` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`natSepDegree_eq_one_iff_of_monic'` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.expand_X` `Polynomial.expand_C`
`natSepDegree_eq_one_iff_of_monic'` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.natSepDegree` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`hasSeparableContraction` `Polynomial.Separable.natSepDegree_eq_natDegree` `Polynomial.natSepDegree_expand` `Polynomial.Monic.eq_X_add_C` `Polynomial.monic_expand_iff` `expChar_pow_pos` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_neg_eq_add` `Polynomial.natSepDegree_X_sub_C`

IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_algebra_isSeparable_of_isSeparable` 📖	—	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	—	`IntermediateField.subset_adjoin` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Polynomial.map_toSubring` `IsScalarTower.left` `IntermediateField.isScalarTower_mid` `IntermediateField.mem_adjoin_simple_self` `Polynomial.aeval_map_algebraMap` `IntermediateField.isScalarTower_bot` `minpoly.aeval` `IsIntegral.tower_top` `isIntegral_trans` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isIntegral` `Polynomial.Separable.of_dvd` `minpoly.dvd` `Field.finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.instIsScalarTowerSubtypeMem_1` `SubsemiringClass.nontrivial` `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable` `IntermediateField.isSeparable_of_mem_isSeparable` `Field.finSepDegree_eq_finrank_iff` `FiniteDimensional.trans` `IntermediateField.finiteDimensional_adjoin` `Finite.of_fintype` `Algebra.IsSeparable.isIntegral` `IntermediateField.adjoin.finiteDimensional` `Module.finrank_mul_finrank` `commRing_strongRankCondition` `Module.Free.of_divisionRing` `Field.finSepDegree_eq_finrank_of_isSeparable` `Algebra.isSeparable_tower_bot_of_isSeparable` `IntermediateField.isScalarTower_mid'`

PerfectField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`splits_of_natSepDegree_eq_one` 📖	mathematical	`Polynomial.natSepDegree`	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map`	—	`perfectField_iff_splits_of_natSepDegree_eq_one` `Polynomial.natSepDegree_map`

Polynomial

Definitions

Name	Category	Theorems
`natSepDegree` 📖	CompOp	44 math math: `natSepDegree_le_natDegree`, `mem_perfectClosure_iff_natSepDegree_eq_one`, `natSepDegree_pow`, `Irreducible.natSepDegree_eq_one_iff_of_monic'`, `Monic.natSepDegree_eq_one_iff_of_irreducible'`, `natSepDegree_X_sub_C_pow`, `minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C`, `Separable.natSepDegree_eq_natDegree`, `natSepDegree_eq_zero_iff`, `natSepDegree_eq_zero`, `natSepDegree_zero`, `IsPurelyInseparable.natSepDegree_eq_one`, `minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow`, `natSepDegree_eq_natDegree_of_separable`, `natSepDegree_C_mul_X_sub_C_pow`, `natSepDegree_X`, `natSepDegree_map`, `HasSeparableContraction.natSepDegree_eq`, `natSepDegree_eq_natDegree_iff`, `natSepDegree_X_pow_char_pow_sub_C`, `isPurelyInseparable_iff_natSepDegree_eq_one`, `Irreducible.natSepDegree_eq_one_iff_of_monic`, `IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree`, `Monic.natSepDegree_eq_one_iff`, `natSepDegree_C_mul`, `natSepDegree_mul_eq_iff`, `natSepDegree_smul_nonzero`, `natSepDegree_expand`, `natSepDegree_pow_of_ne_zero`, `natSepDegree_one`, `IsSeparableContraction.natSepDegree_eq`, `natSepDegree_C`, `Irreducible.natSepDegree_dvd_natDegree`, `minpoly.natSepDegree_eq_one_iff_pow_mem`, `natSepDegree_X_sub_C`, `natSepDegree_eq_of_isAlgClosed`, `natSepDegree_mul_of_isCoprime`, `minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C`, `natSepDegree_mul`, `natSepDegree_eq_of_splits`, `Monic.natSepDegree_eq_one_iff_of_irreducible`, `natSepDegree_X_pow`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one`, `natSepDegree_le_of_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_C` 📖	mathematical	—	`natSepDegree` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`natSepDegree_eq_zero` `natDegree_C`
`natSepDegree_C_mul` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `aroots_C_mul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`natSepDegree_C_mul_X_sub_C_pow` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `X`	—	`natSepDegree_C_mul` `natSepDegree_X_sub_C_pow`
`natSepDegree_X` 📖	mathematical	—	`natSepDegree` `X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`aroots_X` `Multiset.toFinset_singleton` `Finset.card_singleton`
`natSepDegree_X_pow` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`natSepDegree_pow` `natSepDegree_X`
`natSepDegree_X_pow_char_pow_sub_C` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`expand_X` `expand_C` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `natSepDegree_expand` `natSepDegree_X_sub_C`
`natSepDegree_X_sub_C` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`aroots_X_sub_C` `Multiset.toFinset_singleton` `Finset.card_singleton`
`natSepDegree_X_sub_C_pow` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`natSepDegree_pow` `natSepDegree_X_sub_C`
`natSepDegree_eq_natDegree_iff` 📖	mathematical	—	`natSepDegree` `natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Separable` `Semifield.toCommSemiring`	—	`instIsDomain` `card_rootSet_eq_natDegree_iff_of_splits` `SplittingField.splits` `Fintype.card_congr'` `rootSet_def` `Fintype.card_coe`
`natSepDegree_eq_natDegree_of_separable` 📖	mathematical	`Separable` `Semifield.toCommSemiring` `Field.toSemifield`	`natSepDegree` `natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`natSepDegree_eq_natDegree_iff` `Separable.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`natSepDegree_eq_of_isAlgClosed` 📖	mathematical	—	`natSepDegree` `Finset.card` `Multiset.toFinset` `aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield`	—	`natSepDegree_eq_of_splits` `IsAlgClosed.splits`
`natSepDegree_eq_of_splits` 📖	mathematical	`Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	`natSepDegree` `Finset.card` `Multiset.toFinset` `aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain`	—	`instIsDomain` `aroots.eq_1` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `map_map` `Splits.roots_map` `DivisionRing.isSimpleRing` `SplittingField.splits` `Multiset.toFinset_map` `Finset.card_image_of_injective` `RingHom.injective` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `natSepDegree.eq_1`
`natSepDegree_eq_zero` 📖	mathematical	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`natSepDegree`	—	`Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `natSepDegree_le_natDegree` `sub_eq_zero_of_eq`
`natSepDegree_eq_zero_iff` 📖	mathematical	—	`natSepDegree` `natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Function.mtr` `natSepDegree_ne_zero` `natSepDegree_eq_zero`
`natSepDegree_expand` 📖	mathematical	—	`natSepDegree` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid`	—	`one_pow` `expand_one` `instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `roots.congr_simp` `map_expand` `Fintype.card_coe` `Fintype.card_eq` `expChar_prime` `AlgebraicClosure.instCharP` `PerfectField.toPerfectRing` `IsAlgClosed.perfectField`
`natSepDegree_le_natDegree` 📖	mathematical	—	`natSepDegree` `natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`instIsDomain` `card_roots'` `LE.le.trans` `Multiset.toFinset_card_le` `natDegree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `aroots_def`
`natSepDegree_le_of_dvd` 📖	mathematical	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`natSepDegree`	—	`instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `Finset.card_le_card` `Multiset.toFinset_subset` `Multiset.Le.subset` `roots.le_of_dvd` `map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_dvd`
`natSepDegree_map` 📖	mathematical	—	`natSepDegree` `map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `roots.congr_simp` `map_map` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right`
`natSepDegree_mul` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul`	—	`natSepDegree_zero` `Nat.instCanonicallyOrderedAdd` `instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `aroots_mul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Multiset.toFinset_add` `Finset.card_union_le`
`natSepDegree_mul_eq_iff` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul` `instZero` `IsCoprime` `commSemiring` `Semifield.toCommSemiring`	—	`MulZeroClass.zero_mul` `natSepDegree_zero` `zero_add` `isCoprime_zero_left` `isUnit_iff` `IsDomain.to_noZeroDivisors` `instIsDomain` `natSepDegree_eq_zero_iff` `natDegree_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ne.isUnit` `mul_eq_zero` `instNoZeroDivisors` `mul_comm` `add_comm` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `aroots_mul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Multiset.toFinset_add` `isCoprime_of_irreducible_dvd` `instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `IsAlgClosed.exists_aeval_eq_zero` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `degree_pos_of_irreducible` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `MulZeroClass.mul_zero` `add_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AlgHomClass.toRingHomClass` `NeZero.one`
`natSepDegree_mul_of_isCoprime` 📖	mathematical	`IsCoprime` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `commSemiring` `Semifield.toCommSemiring`	`natSepDegree` `instMul`	—	`natSepDegree_mul_eq_iff`
`natSepDegree_ne_zero` 📖	—	—	—	—	`natSepDegree.eq_1` `Finset.card_eq_zero` `Finset.nonempty_iff_ne_empty` `SplittingField.splits` `degree_ne_of_natDegree_ne` `natDegree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Multiset.mem_toFinset` `mem_aroots` `instIsDomain` `IsSplittingField.instIsTorsionFreeSplittingField` `eval_rootOfSplits`
`natSepDegree_ne_zero_iff` 📖	—	—	—	—	`Iff.not` `natSepDegree_eq_zero_iff`
`natSepDegree_one` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instOne`	—	`C_1` `natSepDegree_C`
`natSepDegree_pow` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `aroots_pow` `zero_smul` `Multiset.toFinset_nsmul`
`natSepDegree_pow_of_ne_zero` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`natSepDegree_pow`
`natSepDegree_smul_nonzero` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toSMul` `Semifield.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id`	—	`instIsDomain` `natSepDegree_eq_of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `aroots_smul_nonzero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`natSepDegree_zero` 📖	mathematical	—	`natSepDegree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero`	—	`C_0` `natSepDegree_C`

Polynomial.HasSeparableContraction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_eq` 📖	mathematical	`Polynomial.HasSeparableContraction` `Semifield.toCommSemiring` `Field.toSemifield`	`Polynomial.natSepDegree` `degree`	—	`Polynomial.IsSeparableContraction.natSepDegree_eq` `isSeparableContraction`

Polynomial.IsSeparableContraction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_eq` 📖	mathematical	`Polynomial.IsSeparableContraction` `Semifield.toCommSemiring` `Field.toSemifield`	`Polynomial.natSepDegree` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Polynomial.natSepDegree_expand` `Polynomial.Separable.natSepDegree_eq_natDegree`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.natSepDegree`	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `frobenius` `Semifield.toCommSemiring` `Polynomial.instSub` `Monoid.toNatPow` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`natSepDegree_eq_one_iff_of_irreducible` `one_pow` `pow_one` `not_irreducible_pow` `Nat.Prime.ne_one` `sub_pow_expChar` `expChar_of_injective_ringHom` `Polynomial.C_injective` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `frobenius_def` `pow_mul` `pow_succ` `em`
`eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.natSepDegree`	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `frobenius` `Semifield.toCommSemiring` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`Polynomial.exists_monic_irreducible_factor` `Polynomial.not_isUnit_of_natDegree_pos` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natSepDegree_ne_zero_iff` `LE.le.antisymm` `Polynomial.natSepDegree_le_of_dvd` `ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Irreducible.natDegree_pos` `eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible` `Polynomial.finiteMultiplicity_of_degree_pos_of_monic` `Polynomial.degree_pos_of_irreducible` `multiplicity_pos_of_dvd` `FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd` `Polynomial.eq_one_of_monic_natDegree_zero` `of_mul_monic_left` `pow` `Polynomial.natSepDegree_eq_zero_iff` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Polynomial.natSepDegree_pow_of_ne_zero` `Polynomial.natSepDegree_mul_of_isCoprime` `IsCoprime.pow_left` `Irreducible.isCoprime_or_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `mul_one`
`eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.Splits` `Polynomial.natSepDegree`	`Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`instIsDomain` `Polynomial.Splits.eq_prod_roots_of_monic` `Polynomial.natSepDegree_eq_of_splits` `Polynomial.Splits.map` `Multiset.toFinset_card_eq_one_iff` `Polynomial.map_id` `Algebra.algebraMap_self` `Polynomial.aroots_def` `Multiset.prod_singleton` `Multiset.prod_nsmul` `Multiset.map_singleton` `Multiset.map_nsmul`
`natSepDegree_eq_one_iff` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Polynomial.natSepDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one` `Polynomial.natSepDegree_pow` `Polynomial.natSepDegree_X_pow_char_pow_sub_C`
`natSepDegree_eq_one_iff_of_irreducible` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.natSepDegree` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`Irreducible.natSepDegree_eq_one_iff_of_monic`
`natSepDegree_eq_one_iff_of_irreducible'` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.natSepDegree` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`Irreducible.natSepDegree_eq_one_iff_of_monic'`

Polynomial.Separable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_eq_natDegree` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield`	`Polynomial.natSepDegree` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Polynomial.natSepDegree_eq_natDegree_of_separable`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`perfectField_iff_splits_of_natSepDegree_eq_one` 📖	mathematical	—	`PerfectField` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Polynomial.natSepDegree_zero` `Polynomial.uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `UniqueFactorizationMonoid.factors_prod` `Polynomial.Splits.mul` `Polynomial.Splits.multisetProd` `Polynomial.natSepDegree_le_of_dvd` `UniqueFactorizationMonoid.dvd_of_mem_factors` `Polynomial.Splits.of_natDegree_le_one` `Polynomial.Separable.natSepDegree_eq_natDegree` `UniqueFactorizationMonoid.irreducible_of_factor` `IsUnit.splits` `IsDomain.to_noZeroDivisors` `Units.isUnit` `ExpChar.exists` `PerfectRing.toPerfectField` `PerfectRing.ofSurjective` `isReduced_of_noZeroDivisors` `Polynomial.Splits.exists_eval_eq_zero` `Polynomial.natSepDegree_X_pow_char_pow_sub_C` `pow_one` `LT.lt.ne'` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Nat.cast_pos` `WithBot.instIsOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `WithBot.nontrivial` `expChar_pos` `Polynomial.degree_X_pow_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `sub_eq_zero` `Polynomial.eval_C` `Polynomial.eval_X_pow` `Polynomial.eval_sub`

minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natSepDegree_eq_one_iff_eq_X_pow_sub_C` 📖	mathematical	—	`Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`natSepDegree_eq_one_iff_eq_expand_X_sub_C` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.expand_X` `Polynomial.expand_C`
`natSepDegree_eq_one_iff_eq_X_sub_C_pow` 📖	mathematical	—	`Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `algebraMap` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Nat.instMonoid`	—	`natSepDegree_eq_one_iff_eq_X_pow_sub_C` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.map_C` `sub_eq_zero` `Polynomial.aeval_C` `Polynomial.aeval_X` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `aeval` `RingHom.instRingHomClass` `sub_pow_expChar_pow_of_commute` `expChar_of_injective_ringHom` `Polynomial.C_injective` `expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial` `Polynomial.commute_X` `natSepDegree_eq_one_iff_pow_mem` `map_neg` `RingHomClass.toAddMonoidHomClass` `neg_one_pow_expChar_pow` `neg_pow` `zero_sub` `Polynomial.coeff_C_zero` `Polynomial.coeff_X_zero` `Polynomial.coeff_map` `neg_mul` `one_mul` `neg_neg`
`natSepDegree_eq_one_iff_eq_expand_X_sub_C` 📖	mathematical	—	`Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand` `Monoid.toNatPow` `Nat.instMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`by_contra` `eq_zero` `Polynomial.natSepDegree_zero` `Irreducible.natSepDegree_eq_one_iff_of_monic'` `monic` `irreducible` `instIsDomain` `Polynomial.natSepDegree_expand` `Polynomial.natSepDegree_X_sub_C`
`natSepDegree_eq_one_iff_pow_mem` 📖	mathematical	—	`Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `DivisionRing.toRing` `Field.toDivisionRing` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Polynomial.aeval_C` `Polynomial.aeval_X` `natSepDegree_eq_one_iff_eq_X_pow_sub_C` `aeval` `Polynomial.X_pow_sub_C_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `expChar_pow_pos` `LE.le.antisymm` `LE.le.trans_eq` `Polynomial.natSepDegree_le_of_dvd` `dvd` `Polynomial.natSepDegree_X_pow_char_pow_sub_C` `Polynomial.natSepDegree_ne_zero_iff` `natDegree_pos` `IsDomain.toNontrivial` `IsAlgebraic.isIntegral`

---

← Back to Index