PrimitiveRoots

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

Statistics

Metric	Count
Definitions `zeta`, `embeddingsEquivPrimitiveRoots`, `powerBasis`, `subOnePowerBasis`	4
Theorems `aeval_zeta`, `finrank`, `norm_zeta_eq_one`, `norm_zeta_pow_sub_one_of_prime_ne_two`, `norm_zeta_pow_sub_one_of_prime_pow_ne_two`, `norm_zeta_pow_sub_one_two`, `norm_zeta_sub_one_of_isPrimePow`, `norm_zeta_sub_one_of_prime_ne_two`, `zeta_isRoot`, `zeta_pow`, `zeta_spec`, `dvd_of_isCyclotomicExtension`, `embeddingsEquivPrimitiveRoots_apply_coe`, `exists_neg_pow_of_isOfFinOrder`, `exists_pow_or_neg_mul_pow_of_isOfFinOrder`, `lcm_totient_le_finrank`, `minpoly_sub_one_eq_cyclotomic_comp`, `norm_eq_neg_one_pow`, `norm_eq_one`, `norm_eq_one_of_linearly_ordered`, `norm_of_cyclotomic_irreducible`, `norm_pow_sub_one_eq_prime_pow_of_ne_zero`, `norm_pow_sub_one_of_prime_ne_two`, `norm_pow_sub_one_of_prime_pow_ne_two`, `norm_pow_sub_one_two`, `norm_sub_one_of_prime_ne_two`, `norm_sub_one_of_prime_ne_two'`, `norm_sub_one_two`, `powerBasis_dim`, `powerBasis_gen`, `powerBasis_gen_mem_adjoin_zeta_sub_one`, `subOnePowerBasis_dim`, `subOnePowerBasis_gen`, `sub_one_norm_eq_eval_cyclotomic`, `sub_one_norm_isPrimePow`	35
Total	39

IsCyclotomicExtension

Definitions

Name	Category	Theorems
`zeta` 📖	CompOp	13 math math: `aeval_zeta`, `norm_zeta_pow_sub_one_of_prime_ne_two`, `zeta_pow`, `zeta_isRoot`, `norm_zeta_sub_one_of_prime_ne_two`, `norm_zeta_sub_one_of_isPrimePow`, `zeta_spec`, `norm_zeta_eq_one`, `norm_zeta_pow_sub_one_two`, `fromZetaAut_spec`, `autEquivPow_symm_apply`, `autEquivPow_apply`, `norm_zeta_pow_sub_one_of_prime_pow_ne_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_zeta` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `zeta` `Polynomial.cyclotomic` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Polynomial.eval_map_algebraMap` `Polynomial.IsRoot.def` `Polynomial.map_cyclotomic` `Polynomial.isRoot_cyclotomic_iff` `zeta_spec`
`finrank` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.totient`	—	`zeta_spec` `PowerBasis.finrank` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsPrimitiveRoot.powerBasis_dim` `IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible` `neZero'` `Polynomial.natDegree_cyclotomic`
`norm_zeta_eq_one` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`IsPrimitiveRoot.norm_eq_one` `zeta_spec` `instIsDomain`
`norm_zeta_pow_sub_one_of_prime_ne_two` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `zeta` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`IsPrimitiveRoot.norm_sub_one_of_prime_ne_two` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `zeta_spec`
`norm_zeta_pow_sub_one_of_prime_pow_ne_two` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `zeta` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `zeta_spec`
`norm_zeta_pow_sub_one_two` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`IsPrimitiveRoot.norm_sub_one_two` `zeta_spec`
`norm_zeta_sub_one_of_isPrimePow` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `Nat.minFac`	—	`IsPrimitiveRoot.sub_one_norm_isPrimePow` `zeta_spec`
`norm_zeta_sub_one_of_prime_ne_two` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `zeta` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`IsPrimitiveRoot.norm_sub_one_of_prime_ne_two'` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `zeta_spec`
`zeta_isRoot` 📖	mathematical	—	`Polynomial.IsRoot` `Ring.toSemiring` `CommRing.toRing` `Polynomial.cyclotomic` `zeta`	—	`Polynomial.IsRoot.def` `Polynomial.aeval_def` `Polynomial.eval₂_eq_eval_map` `Polynomial.map_cyclotomic` `aeval_zeta`
`zeta_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`IsPrimitiveRoot.pow_eq_one` `zeta_spec`
`zeta_spec` 📖	mathematical	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `zeta`	—	`exists_isPrimitiveRoot` `Set.mem_singleton`

IsPrimitiveRoot

Definitions

Name	Category	Theorems
`embeddingsEquivPrimitiveRoots` 📖	CompOp	1 math math: `embeddingsEquivPrimitiveRoots_apply_coe`
`powerBasis` 📖	CompOp	10 math math: `IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow`, `IsCyclotomicExtension.discr_odd_prime`, `powerBasis_dim`, `powerBasis_gen_mem_adjoin_zeta_sub_one`, `powerBasis_gen`, `discr_zeta_eq_discr_zeta_sub_one`, `IsCyclotomicExtension.discr_prime_pow_ne_two`, `IsCyclotomicExtension.autEquivPow_symm_apply`, `IsCyclotomicExtension.discr_prime_pow`, `IsCyclotomicExtension.discr_prime_pow_ne_two'`
`subOnePowerBasis` 📖	CompOp	7 math math: `IsCyclotomicExtension.Rat.discr_prime_pow'`, `discr_zeta_eq_discr_zeta_sub_one`, `IsCyclotomicExtension.Rat.discr_prime_pow_ne_two'`, `subOnePowerBasis_dim`, `subOnePowerBasis_gen`, `IsCyclotomicExtension.Rat.discr_odd_prime'`, `IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_isCyclotomicExtension` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—	`NumberField.to_charZero` `IsCyclotomicExtension.zeta_spec` `lcm_totient_le_finrank` `instIsDomain` `NumberField.to_finiteDimensional` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `dvd_lcm_right` `Nat.totient_super_multiplicative` `mul_le_iff_le_one_right` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.totient_pos` `le_trans` `IsCyclotomicExtension.finrank` `MulZeroClass.mul_zero` `Nat.dvd_prime` `Nat.prime_two` `Nat.dvd_two_of_totient_le_one` `mul_one` `dvd_mul_of_dvd_right` `dvd_lcm_left` `mul_comm`
`embeddingsEquivPrimitiveRoots_apply_coe` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `primitiveRoots` `DFunLike.coe` `Equiv` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `embeddingsEquivPrimitiveRoots` `AlgHom.funLike`	—	—
`exists_neg_pow_of_isOfFinOrder` 📖	mathematical	`Odd` `Nat.instSemiring` `IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOfFinOrder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Monoid.toNatPow` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`NumberField.to_charZero` `neg_eq_neg_one_mul` `Commute.orderOf_mul_eq_mul_orderOf_of_coprime` `Commute.all` `orderOf_neg_one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ringChar.eq_zero` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `eq_orderOf` `orderOf` `isOfFinOrder_iff_pow_eq_one` `isRoot_of_unity_iff` `instIsDomain` `NeZero.natCast_ne` `NeZero.charZero` `dvd_of_isCyclotomicExtension` `Polynomial.isRoot_cyclotomic_iff` `pow_mul` `pow_eq_one` `one_pow` `eq_pow_of_pow_eq_one`
`exists_pow_or_neg_mul_pow_of_isOfFinOrder` 📖	mathematical	`Odd` `Nat.instSemiring` `IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOfFinOrder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Monoid.toNatPow` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`NumberField.to_charZero` `exists_neg_pow_of_isOfFinOrder` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `pow_mod_orderOf` `eq_orderOf` `Nat.even_or_odd` `neg_pow` `Even.neg_one_pow` `one_mul` `Odd.neg_one_pow` `neg_mul`
`lcm_totient_le_finrank` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Nat.totient` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Nat.instCanonicallyOrderedAdd` `pow_mul_pow_lcm` `LT.lt.ne'` `IsCyclotomicExtension.finrank` `NeZero.pnat` `Subalgebra.isDomain` `adjoin_isCyclotomicExtension` `Submodule.finrank_le` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`minpoly_sub_one_eq_cyclotomic_comp` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Polynomial.comp` `Polynomial.instAdd` `Polynomial.X` `Polynomial.instOne`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `minpoly.add_algebraMap` `minpoly_eq_cyclotomic_of_irreducible` `IsCyclotomicExtension.neZero'` `sub_neg_eq_add`
`norm_eq_neg_one_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`eq_neg_one_of_two_right` `IsDomain.to_noZeroDivisors` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Algebra.norm_algebraMap`
`norm_eq_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`one_right_iff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.norm_algebraMap` `one_pow` `Nat.two_le_iff` `powerBasis_gen` `Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly` `minpoly_eq_cyclotomic_of_irreducible` `IsCyclotomicExtension.neZero'` `Polynomial.cyclotomic_coeff_zero` `mul_one` `powerBasis_dim` `Polynomial.natDegree_cyclotomic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Even.neg_one_pow` `Nat.totient_even` `LE.le.lt_of_ne`
`norm_eq_one_of_linearly_ordered` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Odd` `Nat.instSemiring`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`iff_def` `StrictMono.injective` `Odd.strictMono_pow` `AddGroup.existsAddOfLE` `one_pow` `map_pow` `MonoidHom.instMonoidHomClass` `Algebra.norm_algebraMap` `RingHom.map_one`
`norm_of_cyclotomic_irreducible` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommRing.toRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidHom.instFunLike` `Algebra.norm` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`norm_eq_neg_one_pow` `IsCyclotomicExtension.finrank` `Nat.cast_one` `norm_eq_one`
`norm_pow_sub_one_eq_prime_pow_of_ne_zero` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`eq_of_prime_pow_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.prime_iff` `Fact.out` `Nat.prime_two` `pow_one` `Nat.pow_right_injective` `Eq.le` `le_antisymm` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instAtLeastTwoHAddOfNat` `norm_pow_sub_one_two` `pow_succ'` `pow_mul` `neg_eq_neg_one_mul` `mul_pow` `neg_one_sq` `one_mul` `norm_pow_sub_one_of_prime_pow_ne_two`
`norm_pow_sub_one_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`norm_pow_sub_one_of_prime_pow_ne_two` `eq_of_prime_pow_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.prime_iff` `Fact.out` `Nat.prime_two` `pow_one`
`norm_pow_sub_one_of_prime_pow_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow` `Fact.out` `instIsDomain` `sub_add_cancel` `pow` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `pow_add` `add_comm` `le_trans` `IsScalarTower.left` `le_antisymm` `IntermediateField.adjoin_simple_le_iff` `add_sub_cancel_right` `sub_mem` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.mem_adjoin_simple_self` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsIntegral.isIntegral` `IsCyclotomicExtension.integral` `IsCyclotomicExtension.equiv` `adjoin_isCyclotomicExtension` `SubsemiringClass.toSubmonoidClass` `coe_submonoidClass_iff` `IsCyclotomicExtension.finiteDimensional` `Finite.of_fintype` `IsCyclotomicExtension.isGalois` `Algebra.norm_eq_norm_adjoin` `sub_one_norm_isPrimePow` `IsPrimePow.pow` `Nat.Prime.isPrimePow` `Nat.pow_minFac` `Nat.Prime.minFac_eq` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IntermediateField.finiteDimensional_left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IntermediateField.finiteDimensional_right` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne'` `tsub_pos_iff_lt` `Nat.instOrderedSub` `Nat.Prime.one_lt` `mul_comm` `mul_assoc` `Nat.totient_prime_pow` `IsCyclotomicExtension.finrank` `tsub_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.Prime.ne_zero`
`norm_pow_sub_one_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`pow_of_dvd` `two_ne_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `pow_dvd_pow` `Nat.instAtLeastTwoHAddOfNat` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_ofNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `eq_neg_one_of_two_right` `IsDomain.to_noZeroDivisors` `instIsDomain` `pow_one` `le_refl` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Algebra.norm_algebraMap` `IsCyclotomicExtension.finrank` `Nat.totient_prime_pow` `Nat.prime_two` `tsub_zero` `Nat.instOrderedSub` `mul_one`
`norm_sub_one_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`pow_zero` `pow_one` `norm_pow_sub_one_of_prime_ne_two`
`norm_sub_one_of_prime_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`zero_add` `pow_one` `norm_sub_one_of_prime_ne_two`
`norm_sub_one_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`pow_one` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `lt_of_lt_of_le` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne` `zero_lt_two` `Polynomial.eval_one_cyclotomic_prime_pow` `Nat.fact_prime_two` `Int.cast_ofNat` `sub_one_norm_eq_eval_cyclotomic`
`powerBasis_dim` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`PowerBasis.dim` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `powerBasis` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly`	—	—
`powerBasis_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `powerBasis`	—	—
`powerBasis_gen_mem_adjoin_zeta_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `powerBasis`	—	`powerBasis_gen` `Algebra.adjoin_singleton_eq_range_aeval` `AlgHom.mem_range` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `sub_add_cancel`
`subOnePowerBasis_dim` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`PowerBasis.dim` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `subOnePowerBasis` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`subOnePowerBasis_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `subOnePowerBasis` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`sub_one_norm_eq_eval_cyclotomic` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddGroupWithOne.toIntCast` `Polynomial.eval` `Int.instRing`	—	`IsAlgClosed.exists_root` `AlgebraicClosure.isAlgClosed` `LT.lt.ne` `Polynomial.degree_cyclotomic_pos` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHom.injective` `DivisionRing.isSimpleRing` `instIsDomain` `IsCyclotomicExtension.finiteDimensional` `Finite.of_fintype` `Algebra.norm_eq_prod_embeddings` `IsGalois.to_isSeparable` `IsCyclotomicExtension.isGalois` `neg_sub` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_sub` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `neg_eq_neg_one_mul` `Finset.prod_mul_distrib` `Finset.prod_const` `Finset.card_univ` `AlgHom.card` `IsCyclotomicExtension.finrank` `Even.neg_one_pow` `Nat.totient_even` `one_mul` `Polynomial.cyclotomic'.eq_1` `Polynomial.eval_prod` `Finset.prod_attach` `Finset.univ_eq_attach` `Fintype.prod_equiv` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `NeZero.of_faithfulSMul` `IsScalarTower.right` `instFaithfulSMul_1` `IsCyclotomicExtension.neZero'` `Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots` `Polynomial.isRoot_cyclotomic_iff` `Polynomial.map_cyclotomic_int` `map_intCast` `RingHom.instRingHomClass` `Int.cast_one` `Polynomial.eval_intCast_map` `eq_intCast`
`sub_one_norm_isPrimePow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsPrimePow` `Nat.instCommMonoidWithZero` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `Nat.minFac`	—	`lt_of_le_of_ne` `IsPrimePow.one_lt` `Nat.minFac_prime` `IsPrimePow.ne_one` `sub_one_norm_eq_eval_cyclotomic` `IsPrimePow.minFac_pow_factorization_eq` `Finsupp.mem_support_toFun` `Nat.mem_primeFactors_iff_mem_primeFactorsList` `Nat.mem_primeFactorsList` `IsPrimePow.ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Fact.out` `Nat.minFac_dvd` `Polynomial.eval_one_cyclotomic_prime_pow` `Int.cast_natCast`

---

← Back to Index