KummerExtension

📁 Source: Mathlib/FieldTheory/KummerExtension.lean

Statistics

Metric	Count
Definitions AdjoinRootXPowSubCEquivToRootsOfUnity, «termK[_√_]», adjoinRootXPowSubCEquiv, autAdjoinRootXPowSubC, autAdjoinRootXPowSubCEquiv, autAdjoinRootXPowSubCHom, autEquivRootsOfUnity, autEquivZmod, rootOfSplitsXPowSubC	9
Theorems adjoin_root_eq_top_of_isSplittingField, adjoin_root_eq_top_of_isSplittingField, separable_X_pow_sub_C_of_irreducible, X_pow_mul_sub_C_irreducible, X_pow_sub_C_eq_prod, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, X_pow_sub_C_irreducible_iff_of_odd, X_pow_sub_C_irreducible_iff_of_prime_pow, X_pow_sub_C_irreducible_of_odd, X_pow_sub_C_irreducible_of_prime_pow, X_pow_sub_C_splits_of_isPrimitiveRoot, adjoinRootXPowSubCEquiv_root, adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_root, autAdjoinRootXPowSubCEquiv_symm_smul, autAdjoinRootXPowSubC_root, autEquivRootsOfUnity_apply_rootOfSplit, autEquivRootsOfUnity_smul, autEquivZmod_symm_apply_intCast, autEquivZmod_symm_apply_natCast, exists_root_adjoin_eq_top_of_isCyclic, finrank_of_isSplittingField_X_pow_sub_C, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, isCyclic_of_isSplittingField_X_pow_sub_C, isCyclic_tfae, isGalois_of_isSplittingField_X_pow_sub_C, isSplittingField_AdjoinRoot_X_pow_sub_C, isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top, rootOfSplitsXPowSubC_pow	29
Total	38

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_root_eq_top_of_isSplittingField 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	adjoin Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain Subalgebra.map_injective AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective map_top AlgHom.range_eq_top AlgEquiv.surjective AlgHom.map_adjoin Set.image_singleton AlgHom.coe_coe adjoinRootXPowSubCEquiv_symm_eq_root AdjoinRoot.adjoinRoot_eq_top

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_root_eq_top_of_isSplittingField 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	adjoin Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain eq_adjoin_of_eq_algebra_adjoin Algebra.adjoin_root_eq_top_of_isSplittingField

KummerExtension

Definitions

Name	Category	Theorems
«termK[_√_]» 📖	CompOp	—

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separable_X_pow_sub_C_of_irreducible 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	Separable Semifield.toCommSemiring	—	instIsDomain ne_zero_of_irreducible_X_pow_sub_C pow_one separable_X_sub_C separable_map IsLocalRing.toNontrivial Field.instIsLocalRing map_sub map_pow map_C map_X AdjoinRoot.algebraMap_eq X_pow_sub_C_eq_prod IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mem_primitiveRoots RingHom.injective DivisionRing.isSimpleRing root_X_pow_sub_C_pow separable_prod_X_sub_C_iff' IsPrimitiveRoot.injOn_pow_mul IsDomain.toIsCancelMulZero root_X_pow_sub_C_ne_zero lt_of_le_of_ne

(root)

Definitions

Name	Category	Theorems
AdjoinRootXPowSubCEquivToRootsOfUnity 📖	CompOp	—
adjoinRootXPowSubCEquiv 📖	CompOp	2 math math: adjoinRootXPowSubCEquiv_symm_eq_root, adjoinRootXPowSubCEquiv_root
autAdjoinRootXPowSubC 📖	CompOp	1 math math: autAdjoinRootXPowSubC_root
autAdjoinRootXPowSubCEquiv 📖	CompOp	2 math math: autAdjoinRootXPowSubCEquiv_root, autAdjoinRootXPowSubCEquiv_symm_smul
autAdjoinRootXPowSubCHom 📖	CompOp	—
autEquivRootsOfUnity 📖	CompOp	2 math math: autEquivRootsOfUnity_apply_rootOfSplit, autEquivRootsOfUnity_smul
autEquivZmod 📖	CompOp	2 math math: autEquivZmod_symm_apply_natCast, autEquivZmod_symm_apply_intCast
rootOfSplitsXPowSubC 📖	CompOp	2 math math: rootOfSplitsXPowSubC_pow, autEquivRootsOfUnity_apply_rootOfSplit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_pow_mul_sub_C_irreducible 📖	—	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField IntermediateField.AdjoinSimple.gen	—	—	Polynomial.not_irreducible_C map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingHom.map_one pow_zero pow_mul Polynomial.sub_comp Polynomial.pow_comp Polynomial.X_comp Polynomial.C_comp Polynomial.irreducible_comp Polynomial.monic_X_pow_sub_C Polynomial.monic_X_pow IsScalarTower.left Polynomial.map_pow Polynomial.map_X
X_pow_sub_C_eq_prod 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial Polynomial.instSub CommRing.toRing Polynomial.semiring Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Finset.prod Polynomial.commRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial Polynomial.map_injective Polynomial.map_sub Polynomial.map_pow Polynomial.map_X Polynomial.map_C Finset.prod_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.map_prod Polynomial.map_mul IsPrimitiveRoot.map_of_injective
X_pow_sub_C_irreducible_iff_forall_prime_of_odd 📖	mathematical	Odd Nat.instSemiring	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	pow_ne_of_irreducible_X_pow_sub_C Nat.Prime.ne_one X_pow_sub_C_irreducible_of_odd
X_pow_sub_C_irreducible_iff_of_odd 📖	mathematical	Odd Nat.instSemiring	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	pow_ne_of_irreducible_X_pow_sub_C X_pow_sub_C_irreducible_of_odd Nat.Prime.ne_one
X_pow_sub_C_irreducible_iff_of_prime_pow 📖	mathematical	Nat.Prime	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X Nat.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	pow_ne_of_irreducible_X_pow_sub_C dvd_pow dvd_rfl Nat.Prime.ne_one X_pow_sub_C_irreducible_of_prime_pow
X_pow_sub_C_irreducible_of_odd 📖	mathematical	Odd Nat.instSemiring	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	induction_on_primes pow_one Polynomial.irreducible_X_sub_C instIsDomain mul_comm X_pow_mul_sub_C_irreducible X_pow_sub_C_irreducible_of_prime dvd_mul_right Polynomial.degree_X_pow_sub_C Nat.Prime.pos IsLocalRing.toNontrivial Field.instIsLocalRing Nat.odd_mul dvd_mul_of_dvd_right IsScalarTower.left map_pow MonoidHom.instMonoidHomClass IntermediateField.adjoin.powerBasis_gen Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly Polynomial.natDegree_sub_C Polynomial.natDegree_pow IsDomain.to_noZeroDivisors Polynomial.natDegree_X mul_one Odd.neg_pow one_pow IntermediateField.minpoly_gen Polynomial.coeff_sub Polynomial.coeff_X_pow Nat.Prime.ne_zero Polynomial.coeff_C_zero zero_sub mul_neg neg_mul one_mul neg_neg
X_pow_sub_C_irreducible_of_prime_pow 📖	mathematical	Nat.Prime	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X Nat.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	X_pow_sub_C_irreducible_of_odd Odd.pow Nat.Prime.odd_of_ne_two Nat.prime_dvd_prime_iff_eq Nat.Prime.dvd_of_dvd_pow
X_pow_sub_C_splits_of_isPrimitiveRoot 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Polynomial.Splits Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.semiring Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	pow_zero RingHom.map_one RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instIsDomain Polynomial.splits_iff_card_roots Polynomial.nthRoots.eq_1 IsPrimitiveRoot.card_nthRoots Polynomial.natDegree_X_pow_sub_C IsLocalRing.toNontrivial Field.instIsLocalRing
adjoinRootXPowSubCEquiv_root 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	AlgEquiv AdjoinRoot CommRing.toCommSemiring AdjoinRoot.instCommRing AdjoinRoot.instAlgebra Algebra.id AlgEquiv.instFunLike adjoinRootXPowSubCEquiv AdjoinRoot.root	—	instIsDomain adjoinRootXPowSubCEquiv.eq_1 AlgEquiv.coe_ofBijective AdjoinRoot.liftAlgHom_root
adjoinRootXPowSubCEquiv_symm_eq_root 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	AlgEquiv AdjoinRoot CommRing.toCommSemiring AdjoinRoot.instCommRing AdjoinRoot.instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm adjoinRootXPowSubCEquiv AdjoinRoot.root	—	instIsDomain AlgEquiv.injective AlgEquiv.apply_symm_apply adjoinRootXPowSubCEquiv_root
autAdjoinRootXPowSubCEquiv_root 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	AlgEquiv AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring Semifield.toCommSemiring AdjoinRoot.instCommRing AdjoinRoot.instAlgebra Algebra.id AlgEquiv.instFunLike MulEquiv Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike autAdjoinRootXPowSubCEquiv AdjoinRoot.root AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Units.val	—	instIsDomain autAdjoinRootXPowSubC_root
autAdjoinRootXPowSubCEquiv_symm_smul 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	Units CommMonoid.toMonoid CommRing.toCommMonoid AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring Units.instSMul AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Semifield.toCommSemiring Algebra.id Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity MulEquiv AlgEquiv AdjoinRoot.instCommRing AdjoinRoot.instAlgebra MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm autAdjoinRootXPowSubCEquiv AdjoinRoot.root AlgEquiv.instFunLike	—	instIsDomain IsScalarTower.right Algebra.smul_def rootsOfUnityEquivOfPrimitiveRoots_symm_apply ite_mul one_mul root_X_pow_sub_C_eq_zero_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass div_mul_cancel₀
autAdjoinRootXPowSubC_root 📖	mathematical	—	DFunLike.coe AlgEquiv AdjoinRoot 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 RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Semifield.toCommSemiring AdjoinRoot.instCommRing AdjoinRoot.instAlgebra Algebra.id AlgEquiv.instFunLike MonoidHom Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AlgEquiv.aut MonoidHom.instFunLike autAdjoinRootXPowSubC AdjoinRoot.root AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Units.val	—	IsScalarTower.right AdjoinRoot.liftAlgHom_root
autEquivRootsOfUnity_apply_rootOfSplit 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	AlgEquiv Semifield.toCommSemiring AlgEquiv.instFunLike rootOfSplitsXPowSubC NeZero.pos AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring CommRing.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgEquiv.aut Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike autEquivRootsOfUnity	—	instIsDomain NeZero.pos Nat.instCanonicallyOrderedAdd MulEquiv.surjective MulEquiv.apply_symm_apply rootOfSplitsXPowSubC_pow autEquivRootsOfUnity.eq_1 adjoinRootXPowSubCEquiv_symm_eq_root IsScalarTower.right autAdjoinRootXPowSubCEquiv_root map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass adjoinRootXPowSubCEquiv_root
autEquivRootsOfUnity_smul 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap	Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.instDistribMulActionSubtypeMem Units.instDistribMulAction Module.toDistribMulAction Ring.toSemiring CommRing.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule MulEquiv AlgEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgEquiv.aut Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike autEquivRootsOfUnity AlgEquiv.instFunLike	—	instIsDomain NeZero.pos Nat.instCanonicallyOrderedAdd IsPrimitiveRoot.nthRoots_eq IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mem_primitiveRoots RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing rootOfSplitsXPowSubC_pow Polynomial.mem_nthRoots map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass autEquivRootsOfUnity_apply_rootOfSplit SMulCommClass.smul_comm Subgroup.smulCommClass_left Units.smulCommClass_left smulCommClass_self
autEquivZmod_symm_apply_intCast 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	AlgEquiv AlgEquiv.instFunLike MulEquiv Multiplicative ZMod Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm autEquivZmod Equiv Equiv.instEquivLike Multiplicative.ofAdd AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing Algebra.toSMul DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	ne_zero_of_irreducible_X_pow_sub_C instIsDomain mem_primitiveRoots autEquivRootsOfUnity_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int MulEquiv.apply_symm_apply Units.val_zpow_eq_zpow_val
autEquivZmod_symm_apply_natCast 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C CommSemiring.toSemiring Semifield.toCommSemiring algebraMap IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	AlgEquiv AlgEquiv.instFunLike MulEquiv Multiplicative ZMod Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm autEquivZmod Equiv Equiv.instEquivLike Multiplicative.ofAdd AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Algebra.toSMul	—	Int.cast_natCast zpow_natCast autEquivZmod_symm_apply_intCast
exists_root_adjoin_eq_top_of_isCyclic 📖	mathematical	Finset.Nonempty primitiveRoots 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 instIsDomain	Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IntermediateField.adjoin Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain orderOf_eq_card_of_forall_mem_zpowers smulCommClass_self IsScalarTower.left minpoly_algEquiv_toLinearMap isOfFinOrder_of_finite Finite.algEquiv Finite.algHom Module.Free.of_divisionRing IsGalois.card_aut_eq_finrank map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_one IsPrimitiveRoot.pow_eq_one mem_primitiveRoots Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.End.HasEigenvalue.exists_hasEigenvector Module.End.hasEigenvalue_of_isRoot Module.End.HasEigenvector.pow_apply IntermediateField.mem_bot OrderIso.map_bot mem_powers_iff_mem_zpowers smul_pow' Submonoid.smul_def AlgEquiv.smul_def smul_pow IsScalarTower.right Algebra.to_smulCommClass pow_mul mul_comm one_pow one_smul OrderIso.injective TopHomClass.map_top InfTopHomClass.toTopHomClass FrameHomClass.toInfTopHomClass CompleteLatticeHomClass.toFrameHomClass OrderIsoClass.toCompleteLatticeHomClass OrderIso.instOrderIsoClass eq_top_iff IntermediateField.mem_adjoin_simple_self IsPrimitiveRoot.dvd_of_pow_eq_one smul_left_injective IsDomain.toIsCancelMulZero pow_card_eq_one' OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass
finrank_of_isSplittingField_X_pow_sub_C 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semifield.toCommSemiring	—	instIsDomain Polynomial.IsSplittingField.finiteDimensional isGalois_of_isSplittingField_X_pow_sub_C ne_zero_of_irreducible_X_pow_sub_C IsGalois.card_aut_eq_finrank Nat.card_congr mem_primitiveRoots Nat.card_zmod
irreducible_X_pow_sub_C_of_root_adjoin_eq_top 📖	mathematical	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap IntermediateField.adjoin Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Irreducible Polynomial Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X Polynomial.C	—	minpoly.unique Polynomial.monic_X_pow_sub_C LT.lt.ne Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Polynomial.eval₂_sub Polynomial.eval₂_X_pow Polynomial.eval₂_C sub_self le_trans Polynomial.degree_X_pow_sub_C Polynomial.degree_eq_natDegree minpoly.ne_zero IsIntegral.of_finite IsScalarTower.left IntermediateField.adjoin.finrank Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero Eq.ge finrank_top Polynomial.degree_le_of_dvd IsDomain.to_noZeroDivisors minpoly.dvd Polynomial.Monic.ne_zero minpoly.irreducible
isCyclic_of_isSplittingField_X_pow_sub_C 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	IsCyclic AlgEquiv Semifield.toCommSemiring DivInvMonoid.toZPow Group.toDivInvMonoid AlgEquiv.aut	—	instIsDomain ne_zero_of_irreducible_X_pow_sub_C isCyclic_of_surjective isCyclic_multiplicative ZMod.instIsAddCyclic MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass mem_primitiveRoots MulEquiv.surjective
isCyclic_tfae 📖	mathematical	Finset.Nonempty primitiveRoots 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 instIsDomain	List.TFAE IsGalois IsCyclic AlgEquiv DivInvMonoid.toZPow Group.toDivInvMonoid AlgEquiv.aut Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.IsSplittingField Set Set.instMembership Set.range CommSemiring.toSemiring algebraMap IntermediateField IntermediateField.adjoin Set.instSingletonSet Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain NeZero.of_pos Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors exists_root_adjoin_eq_top_of_isCyclic irreducible_X_pow_sub_C_of_root_adjoin_eq_top isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top isGalois_of_isSplittingField_X_pow_sub_C isCyclic_of_isSplittingField_X_pow_sub_C List.tfae_of_cycle
isGalois_of_isSplittingField_X_pow_sub_C 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	IsGalois	—	instIsDomain IsGalois.of_separable_splitting_field Polynomial.separable_X_pow_sub_C_of_irreducible
isSplittingField_AdjoinRoot_X_pow_sub_C 📖	mathematical	Finset.Nonempty primitiveRoots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	Polynomial.IsSplittingField AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instField Algebra Semifield.toCommSemiring AdjoinRoot.instAlgebra Algebra.id	—	instIsDomain Polynomial.map_sub Polynomial.map_pow Polynomial.map_C Polynomial.map_X X_pow_sub_C_splits_of_isPrimitiveRoot IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mem_primitiveRoots ne_zero_of_irreducible_X_pow_sub_C RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing root_X_pow_sub_C_pow eq_top_iff AdjoinRoot.adjoinRoot_eq_top Algebra.adjoin_mono Set.singleton_subset_iff Polynomial.mem_rootSet_of_ne instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Polynomial.X_pow_sub_C_ne_zero Polynomial.aeval_def AdjoinRoot.algebraMap_eq AdjoinRoot.eval₂_root
isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top 📖	mathematical	Finset.Nonempty primitiveRoots 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 instIsDomain Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap IntermediateField.adjoin Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Polynomial.IsSplittingField Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.semiring Polynomial.X Polynomial.C	—	instIsDomain Polynomial.map_sub Polynomial.map_pow Polynomial.map_C Polynomial.map_X X_pow_sub_C_splits_of_isPrimitiveRoot IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mem_primitiveRoots Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors RingHom.injective DivisionRing.isSimpleRing eq_top_iff IntermediateField.top_toSubalgebra IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic IsAlgebraic.of_finite Algebra.adjoin_mono Set.singleton_subset_iff Polynomial.mem_rootSet_of_ne Polynomial.X_pow_sub_C_ne_zero Polynomial.aeval_def Polynomial.eval₂_sub Polynomial.eval₂_X_pow Polynomial.eval₂_C sub_self
rootOfSplitsXPowSubC_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield rootOfSplitsXPowSubC NeZero.pos AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike algebraMap	—	Polynomial.IsSplittingField.splits Polynomial.map_sub Polynomial.map_pow Polynomial.map_X Polynomial.map_C Polynomial.degree_X_pow_sub_C NeZero.pos Nat.instCanonicallyOrderedAdd IsLocalRing.toNontrivial Field.instIsLocalRing WithBot.charZero Nat.instCharZero Polynomial.eval_rootOfSplits Polynomial.eval_map Polynomial.eval₂_sub Polynomial.eval₂_X_pow Polynomial.eval₂_C

---

← Back to Index