Basic

📁 Source: Mathlib/NumberTheory/Cyclotomic/Basic.lean

Statistics

Metric	Count
Definitions `CyclotomicField`, `algebra`, `algebraBase`, `instField`, `instInhabited`, `CyclotomicRing`, `algebraBase`, `instAlgebraCyclotomicField`, `instCommRing`, `instInhabited`, `IsCyclotomicExtension`, `algEquiv`	12
Theorems `isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`, `instCharZero`, `instIsCyclotomicExtensionSingletonNatSetOfCharZero`, `instIsCyclotomicExtensionSingletonNatSetOfNat`, `instNumberField`, `isCyclotomicExtension`, `adjoin_algebra_injective`, `algebraBase_injective`, `eq_adjoin_primitive_root`, `instIsDomain`, `instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `instIsScalarTowerCyclotomicField`, `instIsTorsionFreeCyclotomicField`, `instIsTorsionFreeOfIsDomainOfIsFractionRing`, `isCyclotomicExtension`, `isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`, `isCyclotomicExtension_eq`, `isCyclotomicExtension_lcm_sup`, `isCyclotomicExtension_le_of_dvd`, `isCyclotomicExtension_singleton_iff_eq_adjoin`, `adjoin_primitive_root_eq_top`, `adjoin_roots`, `adjoin_roots_cyclotomic_eq_adjoin_nth_roots`, `adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic`, `algEquiv_eq_of_apply_eq`, `eq`, `eq_self_sdiff_zero`, `equiv`, `exists_isPrimitiveRoot`, `finite`, `finiteDimensional`, `finite_of_singleton`, `iff_adjoin_eq_top`, `iff_singleton`, `iff_union_of_dvd`, `iff_union_singleton_one`, `instSubsingleton`, `integral`, `isAbelianGalois`, `isCyclotomicExtension_zero_iff`, `isGalois`, `isMulCommutative`, `isSeparable`, `isSplittingField_X_pow_sub_one`, `lcm_sup`, `le_of_dvd`, `mem_of_pow_eq_one`, `neZero`, `neZero'`, `neZero_of_mem`, `neZero_of_mem'`, `nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot`, `nonempty_algEquiv_adjoin_of_isSepClosed`, `numberField`, `of_union_of_dvd`, `singleton_one`, `singleton_one_of_algebraMap_bijective`, `singleton_one_of_bot_eq_top`, `singleton_zero_of_bot_eq_top`, `splits_X_pow_sub_one`, `splits_cyclotomic`, `splitting_field_cyclotomic`, `subsingleton_iff`, `trans`, `union_left`, `union_of_isPrimitiveRoot`, `union_right`, `adjoin_isCyclotomicExtension`, `intermediateField_adjoin_isCyclotomicExtension`, `isCyclotomicExtension`, `isCyclotomicExtension`, `instIsScalarTowerCyclotomicField`, `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing`, `isCyclotomicExtension_iff`, `isCyclotomicExtension_iff_eq_adjoin`, `isCyclotomicExtension_singleton_iff_eq_adjoin`	76
Total	88

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`IsCyclotomicExtension` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Subalgebra.toCommRing` `Subalgebra.algebra`	—	`subset_adjoin` `Subtype.val_injective` `adjoin_induction` `Subalgebra.algebraMap_mem` `Subalgebra.add_mem` `Subalgebra.mul_mem`

CyclotomicField

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	3 math math: `instIsCyclotomicExtensionSingletonNatSetOfCharZero`, `isCyclotomicExtension`, `instIsCyclotomicExtensionSingletonNatSetOfNat`
`algebraBase` 📖	CompOp	7 math math: `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `CyclotomicRing.instIsScalarTowerCyclotomicField`, `instIsScalarTowerCyclotomicField`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `CyclotomicRing.eq_adjoin_primitive_root`
`instField` 📖	CompOp	15 math math: `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing`, `CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `instNumberField`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `CyclotomicRing.instIsScalarTowerCyclotomicField`, `AddChar.PrimitiveAddChar.prim`, `instIsCyclotomicExtensionSingletonNatSetOfCharZero`, `CyclotomicRing.adjoin_algebra_injective`, `instIsScalarTowerCyclotomicField`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `CyclotomicRing.instIsTorsionFreeCyclotomicField`, `isCyclotomicExtension`, `instIsCyclotomicExtensionSingletonNatSetOfNat`, `instCharZero`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCharZero` 📖	mathematical	—	`CharZero` `CyclotomicField` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`charZero_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instIsCyclotomicExtensionSingletonNatSetOfCharZero` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `CyclotomicField` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `algebra`	—	`instIsCyclotomicExtensionSingletonNatSetOfNat` `isCyclotomicExtension` `NeZero.charZero`
`instIsCyclotomicExtensionSingletonNatSetOfNat` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `CyclotomicField` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `algebra`	—	`Polynomial.isSplittingField_C` `RingHomInvPair.ids` `LinearEquiv.finrank_eq` `Module.finrank_self` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `pow_zero` `Algebra.adjoin_empty` `Subalgebra.bot_eq_top_iff_finrank_eq_one` `Module.Free.of_divisionRing`
`instNumberField` 📖	mathematical	—	`NumberField` `CyclotomicField` `instField`	—	`IsCyclotomicExtension.numberField` `Finite.of_fintype` `instIsCyclotomicExtensionSingletonNatSetOfCharZero` `NumberField.to_charZero`
`isCyclotomicExtension` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `CyclotomicField` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `algebra`	—	`NeZero.nat_of_injective` `RingHom.instRingHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Polynomial.degree_cyclotomic_pos` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Polynomial.Splits.exists_eval_eq_zero` `Polynomial.SplittingField.splits` `Polynomial.degree_map` `Polynomial.isRoot_cyclotomic_iff` `instIsDomain` `Polynomial.map_cyclotomic` `Polynomial.IsRoot.def` `Polynomial.eval_map` `Algebra.eq_top_iff` `Polynomial.SplittingField.adjoin_rootSet` `IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots`

CyclotomicRing

Definitions

Name	Category	Theorems
`algebraBase` 📖	CompOp	4 math math: `instIsTorsionFreeOfIsDomainOfIsFractionRing`, `instIsScalarTowerCyclotomicField`, `algebraBase_injective`, `isCyclotomicExtension`
`instAlgebraCyclotomicField` 📖	CompOp	7 math math: `instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `instIsScalarTowerCyclotomicField`, `adjoin_algebra_injective`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `instIsTorsionFreeCyclotomicField`
`instCommRing` 📖	CompOp	11 math math: `instIsDomain`, `instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `instIsTorsionFreeOfIsDomainOfIsFractionRing`, `instIsScalarTowerCyclotomicField`, `adjoin_algebra_injective`, `algebraBase_injective`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `instIsTorsionFreeCyclotomicField`, `isCyclotomicExtension`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_algebra_injective` 📖	mathematical	—	`CyclotomicRing` `CyclotomicField` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CyclotomicField.instField` `RingHom.instFunLike` `algebraMap` `instAlgebraCyclotomicField`	—	`Subtype.val_injective`
`algebraBase_injective` 📖	mathematical	—	`CyclotomicRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `algebraMap` `algebraBase`	—	`FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `instIsDomain` `instIsTorsionFreeOfIsDomainOfIsFractionRing`
`eq_adjoin_primitive_root` 📖	mathematical	`IsPrimitiveRoot` `CyclotomicField` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField`	`CyclotomicRing` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CyclotomicField.algebraBase` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet`	—	`instIsDomain` `IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic` `IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots`
`instIsDomain` 📖	mathematical	—	`IsDomain` `CyclotomicRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`Subalgebra.isDomain` `instIsDomain`
`instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast` 📖	mathematical	—	`IsFractionRing` `CyclotomicRing` `CommRing.toCommSemiring` `instCommRing` `CyclotomicField` `Semifield.toCommSemiring` `Field.toSemifield` `CyclotomicField.instField` `instAlgebraCyclotomicField`	—	`isUnit_iff_ne_zero` `map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `instIsDomain` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `adjoin_algebra_injective` `NeZero.nat_of_injective` `IsFractionRing.injective` `Algebra.adjoin_induction` `Algebra.subset_adjoin` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `mul_one` `IsLocalization.surj` `map_mem_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `algebraBase_injective` `IsScalarTower.algebraMap_apply` `instIsScalarTowerCyclotomicField` `IsScalarTower.of_algebraMap_eq` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_mem_nonZeroDivisors` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `mul_comm` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `IsCyclotomicExtension.iff_singleton` `CyclotomicField.isCyclotomicExtension`
`instIsScalarTowerCyclotomicField` 📖	mathematical	—	`IsScalarTower` `CyclotomicRing` `CyclotomicField` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRing` `algebraBase` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CyclotomicField.instField` `instAlgebraCyclotomicField` `CyclotomicField.algebraBase`	—	`IsScalarTower.subalgebra'` `IsScalarTower.right`
`instIsTorsionFreeCyclotomicField` 📖	mathematical	—	`Module.IsTorsionFree` `CyclotomicRing` `CyclotomicField` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instAlgebraCyclotomicField`	—	`Module.isTorsionFree_iff_algebraMap_injective` `instIsDomain` `instIsDomain` `adjoin_algebra_injective`
`instIsTorsionFreeOfIsDomainOfIsFractionRing` 📖	mathematical	—	`Module.IsTorsionFree` `CyclotomicRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Algebra.toModule` `algebraBase`	—	`Subalgebra.instIsTorsionFree` `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing`
`isCyclotomicExtension` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `CyclotomicRing` `instCommRing` `algebraBase`	—	`NeZero.of_faithfulSMul` `IsScalarTower.right` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toNontrivial` `instIsDomain` `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing` `IsCyclotomicExtension.exists_isPrimitiveRoot` `CyclotomicField.isCyclotomicExtension` `Set.mem_singleton` `Algebra.subset_adjoin` `isRoot_of_unity_iff` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Nat.mem_divisors_self` `Polynomial.isRoot_cyclotomic_iff` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `IsPrimitiveRoot.coe_submonoidClass_iff` `Set.mem_singleton_iff` `Algebra.adjoin_induction` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.coe_eq_one` `Subalgebra.coe_pow` `Subalgebra.algebraMap_mem` `Subalgebra.add_mem` `Subalgebra.mul_mem`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsCyclotomicExtension` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`Polynomial.Monic.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.monic_X_pow_sub_C` `Polynomial.aeval_sub` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `sub_self` `IsScalarTower.left` `adjoin_toSubalgebra_of_isAlgebraic` `Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`
`isCyclotomicExtension_eq` 📖	—	—	—	—	`IsScalarTower.left` `IsCyclotomicExtension.eq` `instIsDomain`
`isCyclotomicExtension_lcm_sup` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `IsCyclotomicExtension.finite_of_singleton` `instIsDomain` `IsCyclotomicExtension.lcm_sup` `sup_toSubalgebra_of_left`
`isCyclotomicExtension_le_of_dvd` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`IsScalarTower.left` `toSubalgebra_le_toSubalgebra` `IsCyclotomicExtension.le_of_dvd` `instIsDomain`
`isCyclotomicExtension_singleton_iff_eq_adjoin` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `IntermediateField` `SetLike.instMembership` `instSetLike` `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` `adjoin`	—	`IsScalarTower.left` `adjoin_simple_toSubalgebra_of_isAlgebraic` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegral.tower_top` `AddCommGroup.intIsScalarTower` `IsPrimitiveRoot.isIntegral` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `isCyclotomicExtension_singleton_iff_eq_adjoin` `instIsDomain`

IsCyclotomicExtension

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_primitive_root_eq_top` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic` `adjoin_roots_cyclotomic_eq_adjoin_nth_roots` `iff_adjoin_eq_top`
`adjoin_roots` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`adjoin_roots_cyclotomic_eq_adjoin_nth_roots` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Polynomial.rootSet` `Polynomial.cyclotomic` `CommRing.toRing` `setOf` `Set` `Set.instMembership` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`le_antisymm` `Algebra.adjoin_mono` `isRoot_of_unity_iff` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Nat.mem_divisors_self` `Polynomial.IsRoot.def` `Polynomial.map_cyclotomic` `Polynomial.eval_map_algebraMap` `Polynomial.mem_rootSet'` `Algebra.adjoin_le` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `SetLike.mem_coe` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `Polynomial.IsRoot.eq_1` `Polynomial.cyclotomic_ne_zero` `IsDomain.toNontrivial` `IsPrimitiveRoot.isRoot_cyclotomic`
`adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Polynomial.rootSet` `Polynomial.cyclotomic` `CommRing.toRing` `Set` `Set.instSingletonSet`	—	`le_antisymm` `Algebra.adjoin_le` `isRoot_of_unity_iff` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Nat.mem_divisors_self` `Polynomial.IsRoot.eq_1` `Polynomial.map_cyclotomic` `Polynomial.eval_map_algebraMap` `Polynomial.mem_rootSet'` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `SetLike.mem_coe` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin_mono` `Polynomial.cyclotomic_ne_zero` `IsDomain.toNontrivial` `IsPrimitiveRoot.isRoot_cyclotomic`
`algEquiv_eq_of_apply_eq` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgEquiv.instFunLike`	—	—	`AlgEquiv.ext` `adjoin_roots` `Algebra.adjoin_induction` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.commutes` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass`
`eq` 📖	—	—	—	—	`exists_isPrimitiveRoot` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `IsPrimitiveRoot.coe_submonoidClass_iff` `isCyclotomicExtension_iff_eq_adjoin`
`eq_self_sdiff_zero` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	—
`equiv` 📖	mathematical	—	`IsCyclotomicExtension`	—	`iff_union_singleton_one` `trans` `IsScalarTower.of_algHom` `singleton_one_of_algebraMap_bijective` `AlgEquiv.surjective` `AlgEquiv.injective`
`exists_isPrimitiveRoot` 📖	mathematical	`Set` `Set.instMembership`	`IsPrimitiveRoot` `CommRing.toCommMonoid`	—	—
`finite` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Set.Finite.induction_on` `Set.finite_coe_iff` `Module.finite_def` `Finset.coe_singleton` `subsingleton_iff_bot_eq_top` `instSubsingleton` `Algebra.toSubmodule_bot` `Submodule.one_eq_span` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `eq_self_sdiff_zero` `union_left` `Set.subset_insert` `Subalgebra.isDomain` `union_right` `Set.union_singleton` `finite_of_singleton` `Module.Finite.trans` `IsScalarTower.subalgebra'` `IsScalarTower.right`
`finiteDimensional` 📖	mathematical	—	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`finite`
`finite_of_singleton` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Module.finite_def` `Algebra.top_toSubmodule` `iff_adjoin_eq_top` `fg_adjoin_of_finite` `Set.ext` `Finset.finite_toSet` `Polynomial.monic_X_pow_sub_C` `Polynomial.eval₂_sub` `Polynomial.eval₂_X_pow` `Polynomial.eval₂_one`
`iff_adjoin_eq_top` 📖	mathematical	—	`IsCyclotomicExtension` `IsPrimitiveRoot` `CommRing.toCommMonoid` `Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`exists_isPrimitiveRoot` `Algebra.eq_top_iff` `adjoin_roots`
`iff_singleton` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `IsPrimitiveRoot` `CommRing.toCommMonoid` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `setOf` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`iff_union_of_dvd` 📖	mathematical	`Set` `Set.instMembership`	`IsCyclotomicExtension` `Set.instUnion` `Set.instSingletonSet`	—	`of_union_of_dvd` `iff_adjoin_eq_top` `exists_isPrimitiveRoot` `Set.subset_union_left` `eq_top_iff` `Algebra.adjoin_mono` `Set.union_singleton` `pow_mul` `one_pow`
`iff_union_singleton_one` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instUnion` `Set.instSingletonSet`	—	`iff_union_of_dvd` `Unique.instSubsingleton` `eq_self_sdiff_zero` `Set.union_diff_distrib` `Set.ext` `Set.empty_union` `Set.diff_singleton_eq_self` `iff_adjoin_eq_top` `Set.mem_singleton_iff` `pow_one` `Algebra.adjoin_singleton_one` `subsingleton_iff_bot_eq_top` `instSubsingleton` `Set.notMem_empty` `Algebra.adjoin_empty` `singleton_one`
`instSubsingleton` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`subsingleton_of_bot_eq_top` `instIsEmptyFalse` `Algebra.adjoin_empty`
`integral` 📖	mathematical	—	`Algebra.IsIntegral` `CommRing.toRing`	—	`AlgEquiv.isIntegral_iff` `iff_adjoin_eq_top` `Algebra.IsIntegral.adjoin` `Polynomial.monic_X_pow_sub_C` `Polynomial.eval₂_sub` `Polynomial.eval₂_X_pow` `Polynomial.eval₂_one` `sub_self`
`isAbelianGalois` 📖	mathematical	—	`IsAbelianGalois`	—	`isGalois` `isMulCommutative` `instIsDomain`
`isCyclotomicExtension_zero_iff` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.surjective_algebraMap_iff` `eq_self_sdiff_zero` `sdiff_self` `Set.bot_eq_empty` `subsingleton_iff_bot_eq_top` `instSubsingleton` `singleton_zero_of_bot_eq_top`
`isGalois` 📖	mathematical	—	`IsGalois`	—	`isGalois_iff` `isSeparable` `IsScalarTower.left` `nonempty_algEquiv_adjoin_of_isSepClosed` `IsSepClosed.of_isAlgClosed` `AlgebraicClosure.isAlgClosed` `AlgEquiv.transfer_normal` `IntermediateField.normal_iff_forall_map_le` `IsAlgClosure.normal` `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.isSeparable_self` `Subalgebra.mem_map` `IntermediateField.toSubalgebra_map` `IntermediateField.mem_toSubalgebra` `IntermediateField.adjoin_induction` `IntermediateField.subset_adjoin` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `AlgHom.commutes` `IntermediateField.algebraMap_mem` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `map_inv₀` `InvMemClass.inv_mem` `SubfieldClass.toInvMemClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass`
`isMulCommutative` 📖	mathematical	—	`IsMulCommutative` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut`	—	`algEquiv_eq_of_apply_eq` `exists_isPrimitiveRoot` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsPrimitiveRoot.pow_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `mul_comm`
`isSeparable` 📖	mathematical	—	`Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`integral` `iff_adjoin_eq_top` `IsScalarTower.left` `AlgEquiv.Algebra.isSeparable_iff` `IntermediateField.toSubalgebra_injective` `IntermediateField.top_toSubalgebra` `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic` `Algebra.IsAlgebraic.isAlgebraic` `Algebra.IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isSeparable_adjoin_iff_isSeparable` `Polynomial.X_pow_sub_one_separable_iff` `neZero_of_mem'` `instIsDomain` `Polynomial.Separable.of_dvd` `minpoly.dvd` `Polynomial.aeval_sub` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `sub_self`
`isSplittingField_X_pow_sub_one` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instOne`	—	`splits_X_pow_sub_one` `Set.mem_singleton` `instIsDomain` `iff_adjoin_eq_top` `Set.ext` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.map_one` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Polynomial.aeval_X` `Polynomial.aeval_one` `Polynomial.X_pow_sub_C_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NeZero.pos` `Nat.instCanonicallyOrderedAdd`
`lcm_sup` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Subalgebra.toCommRing` `Subalgebra.algebra`	—	`exists_isPrimitiveRoot` `IsPrimitiveRoot.map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `IsPrimitiveRoot.pow_mul_pow_lcm` `sup_comm` `isCyclotomicExtension_singleton_iff_eq_adjoin` `Algebra.adjoin_union` `Set.union_singleton` `IsPrimitiveRoot.adjoin_pair_eq` `IsPrimitiveRoot.adjoin_isCyclotomicExtension`
`le_of_dvd` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder`	—	`eq_zero_of_zero_dvd` `exists_isPrimitiveRoot` `IsPrimitiveRoot.map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `IsPrimitiveRoot.pow` `mul_comm` `isCyclotomicExtension_singleton_iff_eq_adjoin` `Algebra.adjoin_le` `Set.singleton_subset_iff` `Subalgebra.pow_mem` `Algebra.self_mem_adjoin_singleton`
`mem_of_pow_eq_one` 📖	mathematical	`Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike`	—	`exists_isPrimitiveRoot` `IsPrimitiveRoot.map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `map_pow` `Subalgebra.pow_mem` `Subtype.prop`
`neZero` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`neZero_of_mem` `Set.mem_singleton`
`neZero'` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`neZero_of_mem'` `Set.mem_singleton`
`neZero_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`IsPrimitiveRoot.neZero'` `exists_isPrimitiveRoot`
`neZero_of_mem'` 📖	mathematical	`Set` `Set.instMembership`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`NeZero.nat_of_neZero` `RingHom.instRingHomClass` `neZero_of_mem`
`nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Semifield.toCommSemiring` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`
`nonempty_algEquiv_adjoin_of_isSepClosed` 📖	mathematical	—	`AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Semifield.toCommSemiring` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`isSeparable` `IsScalarTower.left` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `le_antisymm` `iff_adjoin_eq_top` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Subalgebra.ext` `AlgEquiv.apply_symm_apply` `AlgHom.mem_range` `Algebra.adjoin_induction` `Algebra.subset_adjoin` `IntermediateField.subset_adjoin` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `Subtype.val_injective` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `Subalgebra.instSMulMemClass` `AlgHom.commutes` `IntermediateField.algebraMap_mem` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `IntermediateField.adjoin_le_iff` `exists_isPrimitiveRoot` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `instIsDomain` `IsPrimitiveRoot.map_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing`
`numberField` 📖	mathematical	—	`NumberField`	—	`charZero_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NumberField.to_charZero` `Module.Finite.trans` `IsScalarTower.rat` `NumberField.to_finiteDimensional` `finite` `instIsDomain`
`of_union_of_dvd` 📖	mathematical	`Set` `Set.instMembership`	`IsCyclotomicExtension` `Set.instUnion` `Set.instSingletonSet`	—	`iff_adjoin_eq_top` `Set.mem_singleton_iff` `Set.mem_union` `exists_isPrimitiveRoot` `IsPrimitiveRoot.pow_of_dvd` `dvd_mul_left` `mul_div_cancel_right₀` `Nat.instMulDivCancelClass` `eq_top_iff` `Algebra.adjoin_mono` `Set.union_singleton`
`singleton_one` 📖	mathematical	—	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`Algebra.eq_top_iff` `pow_one` `Algebra.adjoin_singleton_one` `isCyclotomicExtension_iff`
`singleton_one_of_algebraMap_bijective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet`	—	`singleton_one_of_bot_eq_top` `Algebra.surjective_algebraMap_iff`
`singleton_one_of_bot_eq_top` 📖	mathematical	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet`	—	`Set.union_singleton` `Set.insert_diff_eq_singleton` `iff_union_singleton_one` `singleton_zero_of_bot_eq_top` `eq_self_sdiff_zero`
`singleton_zero_of_bot_eq_top` 📖	mathematical	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet`	—	`iff_adjoin_eq_top` `instIsEmptyFalse` `pow_zero` `Algebra.adjoin_empty`
`splits_X_pow_sub_one` 📖	mathematical	`Set` `Set.instMembership`	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instOne`	—	`Polynomial.map_sub` `Polynomial.map_one` `Polynomial.map_pow` `Polynomial.map_X` `isCyclotomicExtension_iff` `Polynomial.X_pow_sub_one_splits`
`splits_cyclotomic` 📖	mathematical	`Set` `Set.instMembership`	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `Polynomial.cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Polynomial.Splits.of_dvd` `instIsDomain` `splits_X_pow_sub_one` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.X_pow_sub_C_ne_zero` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Polynomial.map_dvd_map'` `Polynomial.eq_cyclotomic_iff`
`splitting_field_cyclotomic` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial.cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing`	—	`splits_cyclotomic` `Set.mem_singleton` `instIsDomain` `iff_adjoin_eq_top` `exists_isPrimitiveRoot` `adjoin_roots_cyclotomic_eq_adjoin_nth_roots`
`subsingleton_iff` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instHasSubset` `Set.instInsert` `Set.instSingletonSet`	—	`Subalgebra.subsingleton_of_subsingleton` `Set.subset_pair_iff` `IsPrimitiveRoot.unique` `IsPrimitiveRoot.of_subsingleton` `Lean.Meta.FastSubsingleton.elim` `Algebra.mem_top`
`trans` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsCyclotomicExtension` `Set` `Set.instUnion`	—	`isCyclotomicExtension_iff` `IsPrimitiveRoot.map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.adjoin_induction` `Algebra.subset_adjoin` `Algebra.adjoin_mono` `Set.mem_union_left` `map_pow` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `Algebra.adjoin_image` `IsScalarTower.toAlgHom_apply` `Subalgebra.add_mem` `Subalgebra.mul_mem`
`union_left` 📖	mathematical	`Set` `Set.instHasSubset`	`IsCyclotomicExtension` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `setOf` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Subalgebra.toCommRing` `Subalgebra.algebra`	—	`isCyclotomicExtension_iff` `Algebra.subset_adjoin` `IsPrimitiveRoot.pow_eq_one` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `IsPrimitiveRoot.coe_submonoidClass_iff` `Algebra.adjoin_adjoin_coe_preimage` `Set.preimage_setOf_eq` `Nat.cast_one` `Algebra.mem_top`
`union_of_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`IsCyclotomicExtension` `Set` `Set.instUnion` `Set.instSingletonSet`	—	`eq_self_sdiff_zero` `Set.union_diff_right` `iff_adjoin_eq_top` `exists_isPrimitiveRoot` `le_antisymm` `Set.union_singleton` `Algebra.adjoin_mono`
`union_right` 📖	mathematical	—	`IsCyclotomicExtension` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`le_antisymm` `isCyclotomicExtension_iff` `Set.mem_union_right` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Subalgebra.mem_restrictScalars` `Algebra.adjoin_union_eq_adjoin_adjoin`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_isCyclotomicExtension` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Polynomial.instCommRingAdjoinSingleton` `CommRing.toRing` `Subalgebra.algebra`	—	`Algebra.subset_adjoin` `Set.mem_singleton` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `coe_submonoidClass_iff` `Set.mem_singleton_iff` `Algebra.adjoin_induction` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.coe_eq_one` `Subalgebra.coe_pow` `iff_def` `Subalgebra.algebraMap_mem` `Subalgebra.add_mem` `Subalgebra.mul_mem`
`intermediateField_adjoin_isCyclotomicExtension` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `IntermediateField.toField` `IntermediateField.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` `IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic` `Algebra.IsAlgebraic.isAlgebraic` `Algebra.IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `adjoin_isCyclotomicExtension`

IsSepClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclotomicExtension` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`IsCyclotomicExtension` `Algebra.id` `CommRing.toCommSemiring`	—	`exists_aeval_eq_zero` `instFaithfulSMul_1` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Polynomial.degree_cyclotomic_pos` `Polynomial.separable_cyclotomic` `Polynomial.isRoot_cyclotomic_iff` `instIsDomain` `Polynomial.IsRoot.def` `Polynomial.coe_aeval_eq_eval` `Algebra.eq_top_iff` `Unique.instSubsingleton`

IsSepClosedOfCharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclotomicExtension` 📖	mathematical	—	`IsCyclotomicExtension` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.id` `CommRing.toCommSemiring`	—	`IsCyclotomicExtension.eq_self_sdiff_zero` `IsSepClosed.isCyclotomicExtension` `Nat.cast_ne_zero`

(root)

Definitions

Name	Category	Theorems
`CyclotomicField` 📖	CompOp	15 math math: `instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing`, `CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `CyclotomicField.instNumberField`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `CyclotomicRing.instIsScalarTowerCyclotomicField`, `AddChar.PrimitiveAddChar.prim`, `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero`, `CyclotomicRing.adjoin_algebra_injective`, `instIsScalarTowerCyclotomicField`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `CyclotomicRing.instIsTorsionFreeCyclotomicField`, `CyclotomicField.isCyclotomicExtension`, `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfNat`, `CyclotomicField.instCharZero`
`CyclotomicRing` 📖	CompOp	12 math math: `CyclotomicRing.instIsDomain`, `CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `CyclotomicRing.instIsTorsionFreeOfIsDomainOfIsFractionRing`, `CyclotomicRing.instIsScalarTowerCyclotomicField`, `CyclotomicRing.adjoin_algebra_injective`, `CyclotomicRing.algebraBase_injective`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `CyclotomicRing.instIsTorsionFreeCyclotomicField`, `CyclotomicRing.isCyclotomicExtension`, `CyclotomicRing.eq_adjoin_primitive_root`
`IsCyclotomicExtension` 📖	CompData	35 math math: `IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin`, `IsCyclotomicExtension.iff_union_of_dvd`, `IsCyclotomicExtension.isCyclotomicExtension_zero_iff`, `IsSepClosedOfCharZero.isCyclotomicExtension`, `IsCyclotomicExtension.singleton_zero_of_bot_eq_top`, `Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`, `IntermediateField.isCyclotomicExtension_lcm_sup`, `IsCyclotomicExtension.subsingleton_iff`, `IsCyclotomicExtension.singleton_one_of_algebraMap_bijective`, `isCyclotomicExtension_iff_eq_adjoin`, `IsSepClosed.isCyclotomicExtension`, `IsCyclotomicExtension.ring_of_integers'`, `IsCyclotomicExtension.ringOfIntegers`, `IsCyclotomicExtension.union_of_isPrimitiveRoot`, `IsCyclotomicExtension.iff_singleton`, `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero`, `IsCyclotomicExtension.of_union_of_dvd`, `IsCyclotomicExtension.trans`, `isCyclotomicExtension_singleton_iff_eq_adjoin`, `IsCyclotomicExtension.union_left`, `IsCyclotomicExtension.equiv`, `isCyclotomicExtension_iff`, `IsCyclotomicExtension.iff_adjoin_eq_top`, `IsCyclotomicExtension.eq_self_sdiff_zero`, `IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow`, `IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`, `CyclotomicField.isCyclotomicExtension`, `CyclotomicRing.isCyclotomicExtension`, `IsCyclotomicExtension.singleton_one_of_bot_eq_top`, `IsPrimitiveRoot.adjoin_isCyclotomicExtension`, `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfNat`, `IsCyclotomicExtension.union_right`, `IsCyclotomicExtension.iff_union_singleton_one`, `IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension`, `IsCyclotomicExtension.lcm_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerCyclotomicField` 📖	mathematical	—	`IsScalarTower` `CyclotomicField` `Algebra.toSMul` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `CyclotomicField.algebraBase` `Algebra.id`	—	—
`instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing` 📖	mathematical	—	`Module.IsTorsionFree` `CyclotomicField` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CyclotomicField.algebraBase`	—	`Module.isTorsionFree_iff_faithfulSMul` `instIsDomain` `faithfulSMul_iff_algebraMap_injective` `IsScalarTower.algebraMap_eq` `instIsScalarTowerCyclotomicField` `FaithfulSMul.algebraMap_injective` `instFaithfulSMul_1` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsFractionRing.injective`
`isCyclotomicExtension_iff` 📖	mathematical	—	`IsCyclotomicExtension` `IsPrimitiveRoot` `CommRing.toCommMonoid` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`isCyclotomicExtension_iff_eq_adjoin` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`IsCyclotomicExtension` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommRing` `Subalgebra.algebra` `Algebra.adjoin` `setOf` `Set` `Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`IsCyclotomicExtension.iff_adjoin_eq_top` `Subalgebra.range_val` `Algebra.map_top` `AlgHom.map_adjoin` `Set.ext` `Set.image_congr` `IsCyclotomicExtension.mem_of_pow_eq_one` `Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`
`isCyclotomicExtension_singleton_iff_eq_adjoin` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommRing` `Subalgebra.algebra` `Algebra.adjoin`	—	`isCyclotomicExtension_iff_eq_adjoin` `le_antisymm` `Algebra.adjoin_le` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `Subalgebra.pow_mem` `Algebra.self_mem_adjoin_singleton` `Algebra.adjoin_mono` `Set.singleton_subset_iff` `IsPrimitiveRoot.pow_eq_one`

---

← Back to Index