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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing 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.toPow Nat.instMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne zeta Monoid.toPow Nat.instMonoid 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.toPow Nat.instMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield zeta Nat.instMonoid 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.toPow Nat.instMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne zeta Monoid.toPow Nat.instMonoid 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing 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.toPow 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.toPow 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	—	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.toPow 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	—	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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing Polynomial.cyclotomic Polynomial 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.toPow 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 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	—	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 Ring.toSemiring 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 DivisionRing.toRing Field.toDivisionRing 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Nat.instMonoid 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Nat.instMonoid 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Nat.instMonoid 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Nat.instMonoid 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain 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.toPow 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast Polynomial.eval Int.instRing Polynomial.cyclotomic	—	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 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain 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