Basic

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

Statistics

Metric	Count
Definitions `adjoinEquivRingOfIntegers`, `adjoinEquivRingOfIntegersOfPrimePow`, `integralPowerBasis`, `integralPowerBasis'`, `integralPowerBasisOfPrimePow`, `subOneIntegralPowerBasis`, `subOneIntegralPowerBasis'`, `subOneIntegralPowerBasisOfPrimePow`, `toInteger`	9
Theorems `absdiscr_prime`, `absdiscr_prime_pow`, `absdiscr_prime_pow_succ`, `adjoin_singleton_eq_top`, `cyclotomicRing_isIntegralClosure`, `cyclotomicRing_isIntegralClosure_of_prime`, `cyclotomicRing_isIntegralClosure_of_prime_pow`, `discr`, `discr_odd_prime'`, `discr_prime`, `discr_prime_pow`, `discr_prime_pow'`, `discr_prime_pow_eq_unit_mul_pow'`, `discr_prime_pow_ne_two'`, `discr_prime_pow_succ`, `finrank`, `isIntegralClosure_adjoin_singleton`, `isIntegralClosure_adjoin_singleton_of_prime`, `isIntegralClosure_adjoin_singleton_of_prime_pow`, `natAbs_discr`, `torsionOrder_eq`, `ringOfIntegers`, `ring_of_integers'`, `ringOfIntegersOfPrimePow`, `adjoinEquivRingOfIntegersOfPrimePow_apply`, `adjoinEquivRingOfIntegersOfPrimePow_symm_apply`, `adjoinEquivRingOfIntegers_apply`, `adjoinEquivRingOfIntegers_symm_apply`, `card_quotient_toInteger_sub_one`, `coe_toInteger`, `finite_quotient_span_sub_one`, `finite_quotient_span_sub_one'`, `finite_quotient_toInteger_sub_one`, `integralPowerBasis'_gen`, `integralPowerBasisOfPrimePow_dim`, `integralPowerBasisOfPrimePow_gen`, `integralPowerBasis_dim`, `integralPowerBasis_gen`, `norm_toInteger_pow_sub_one_of_prime_ne_two`, `norm_toInteger_pow_sub_one_of_prime_pow_ne_two`, `norm_toInteger_pow_sub_one_of_two`, `norm_toInteger_sub_one_eq_one`, `norm_toInteger_sub_one_of_eq_two`, `norm_toInteger_sub_one_of_eq_two_pow`, `norm_toInteger_sub_one_of_prime_ne_two`, `norm_toInteger_sub_one_of_prime_ne_two'`, `not_exists_int_prime_dvd_sub_of_prime_ne_two`, `not_exists_int_prime_dvd_sub_of_prime_ne_two'`, `not_exists_int_prime_dvd_sub_of_prime_pow_ne_two`, `power_basis_int'_dim`, `prime_dvd_of_dvd_norm_sub_one`, `prime_norm_toInteger_sub_one_of_prime_ne_two`, `prime_norm_toInteger_sub_one_of_prime_ne_two'`, `prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `subOneIntegralPowerBasis'_gen`, `subOneIntegralPowerBasis'_gen_prime`, `subOneIntegralPowerBasisOfPrimePow_gen`, `subOneIntegralPowerBasisOfPrimePow_gen_prime`, `subOneIntegralPowerBasis_gen`, `subOneIntegralPowerBasis_gen_prime`, `toInteger_isPrimitiveRoot`, `toInteger_sub_one_dvd_prime`, `toInteger_sub_one_dvd_prime'`, `toInteger_sub_one_not_dvd_two`, `zeta_sub_one_prime`, `zeta_sub_one_prime'`, `zeta_sub_one_prime_of_ne_two`, `zeta_sub_one_prime_of_two_pow`, `dvd_torsionOrder_of_isPrimitiveRoot`	69
Total	78

IsCyclotomicExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ringOfIntegers` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `NumberField.RingOfIntegers` `Int.instCommRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing`	—	`IsPrimitiveRoot.adjoin_isCyclotomicExtension` `zeta_spec` `equiv`
`ring_of_integers'` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `NumberField.RingOfIntegers` `Int.instCommRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing`	—	`ringOfIntegers`

IsCyclotomicExtension.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absdiscr_prime` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Monoid.toNatPow` `Int.instMonoid`	—	`discr_prime`
`absdiscr_prime_pow` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `Nat.instMonoid` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Int.instMonoid` `Nat.totient`	—	`discr_prime_pow`
`absdiscr_prime_pow_succ` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `Nat.instMonoid` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Int.instMonoid`	—	`discr_prime_pow_succ`
`adjoin_singleton_eq_top` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Algebra.adjoin` `NumberField.RingOfIntegers` `Int.instCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing` `Set` `Set.instSingletonSet` `IsPrimitiveRoot.toInteger` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`PowerBasis.adjoin_gen_eq_top` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen` `NeZero.of_gt` `IsPrimitiveRoot.pow` `NeZero.pos` `mul_comm` `IsScalarTower.left` `IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `NumberField.to_finiteDimensional` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsPrimitiveRoot.coe_submonoidClass_iff` `IntermediateField.charZero` `Rat.instCharZero` `NumberField.of_intermediateField` `Rat.numberField` `IsCyclotomicExtension.equiv` `Nat.Coprime.lcm_eq_mul` `IntermediateField.isCyclotomicExtension_lcm_sup` `IntermediateField.isCyclotomicExtension_eq` `IsCyclotomicExtension.numberField` `Finite.of_fintype`
`cyclotomicRing_isIntegralClosure` 📖	mathematical	—	`IsIntegralClosure` `CyclotomicRing` `Int.instCommRing` `Rat.instField` `Ring.toIntAlgebra` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `CyclotomicField` `CommRing.toCommSemiring` `CyclotomicRing.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `CyclotomicField.algebraBase` `CyclotomicRing.instAlgebraCyclotomicField`	—	`CyclotomicField.instCharZero` `Rat.instCharZero` `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero` `IsCyclotomicExtension.zeta_spec` `IsFractionRing.injective` `CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast` `Rat.isFractionRing` `Int.instIsDomain` `IsIntegralClosure.isIntegral_iff` `isIntegralClosure_adjoin_singleton` `Algebra.adjoin_mono` `IsPrimitiveRoot.pow_eq_one` `IsIntegral.algebraMap` `AddCommGroup.intIsScalarTower` `Algebra.IsIntegral.isIntegral` `IsCyclotomicExtension.integral` `CyclotomicRing.isCyclotomicExtension`
`cyclotomicRing_isIntegralClosure_of_prime` 📖	mathematical	—	`IsIntegralClosure` `CyclotomicRing` `Int.instCommRing` `Rat.instField` `Ring.toIntAlgebra` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `CyclotomicField` `CommRing.toCommSemiring` `CyclotomicRing.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `CyclotomicField.algebraBase` `CyclotomicRing.instAlgebraCyclotomicField`	—	`pow_one` `cyclotomicRing_isIntegralClosure_of_prime_pow`
`cyclotomicRing_isIntegralClosure_of_prime_pow` 📖	mathematical	—	`IsIntegralClosure` `CyclotomicRing` `Monoid.toNatPow` `Nat.instMonoid` `Int.instCommRing` `Rat.instField` `Ring.toIntAlgebra` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `CyclotomicField` `CommRing.toCommSemiring` `CyclotomicRing.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CyclotomicField.instField` `CyclotomicField.algebraBase` `CyclotomicRing.instAlgebraCyclotomicField`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `CyclotomicField.instCharZero` `Rat.instCharZero` `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero` `IsCyclotomicExtension.zeta_spec` `IsFractionRing.injective` `CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast` `Rat.isFractionRing` `Int.instIsDomain` `IsIntegralClosure.isIntegral_iff` `isIntegralClosure_adjoin_singleton_of_prime_pow` `Algebra.adjoin_mono` `IsPrimitiveRoot.pow_eq_one` `IsIntegral.algebraMap` `AddCommGroup.intIsScalarTower` `Algebra.IsIntegral.isIntegral` `IsCyclotomicExtension.integral` `CyclotomicRing.isCyclotomicExtension`
`discr` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Monoid.toNatPow` `Int.instMonoid` `Nat.totient` `Finset.prod` `Nat.instCommMonoid` `Nat.primeFactors` `Nat.instMonoid`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `NumberField.sign_discr` `nrComplexPlaces_eq_totient_div_two` `discr_prime_pow` `pow_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MulZeroClass.mul_zero` `mul_one` `Int.natAbs_of_isUnit` `one_pow` `Finset.prod_congr` `Nat.primeFactors_one` `Nat.instZeroLEOneClass` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `one_mul` `Nat.prime_pow_pow_totient_ediv_prod` `NeZero.of_gt` `IsCyclotomicExtension.zeta_spec` `IsPrimitiveRoot.pow` `NeZero.pos` `mul_comm` `IsScalarTower.left` `IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `NumberField.to_finiteDimensional` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsPrimitiveRoot.coe_submonoidClass_iff` `NumberField.of_intermediateField` `IntermediateField.charZero` `Rat.instCharZero` `IsCyclotomicExtension.isGalois` `IsCyclotomicExtension.equiv` `Nat.Coprime.lcm_eq_mul` `IntermediateField.isCyclotomicExtension_lcm_sup` `IntermediateField.isCyclotomicExtension_eq` `Int.isCoprime_iff_nat_coprime` `Nat.prod_primeFactors_pow_totient_ediv_dvd` `IsScalarTower.rat` `NumberField.linearDisjoint_of_isGalois_isCoprime_discr` `NumberField.to_charZero` `NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow` `NumberField.isCoprime_differentIdeal_of_isCoprime_discr` `finrank` `pow_dvd_pow_of_dvd` `Nat.primeFactors_mul` `Finset.prod_union` `Nat.Coprime.disjoint_primeFactors` `Finset.prod_pow` `Nat.totient_dvd_of_dvd` `Nat.totient_prime` `Nat.prime_of_mem_primeFactors` `Nat.dvd_of_mem_primeFactors` `Nat.totient_mul` `mul_pow`
`discr_odd_prime'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Algebra.discr` `PowerBasis.dim` `Rat.instField` `CommRing.toRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `IsPrimitiveRoot.subOnePowerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Rat.commRing` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Module.Basis.instFunLike` `PowerBasis.basis`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `IsCyclotomicExtension.discr_odd_prime` `Polynomial.cyclotomic.irreducible_rat` `Nat.Prime.pos` `Fact.out` `IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one`
`discr_prime` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Monoid.toNatPow` `Int.instMonoid`	—	`zero_add` `pow_one` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `discr_prime_pow_succ` `pow_zero` `one_mul` `mul_one`
`discr_prime_pow` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `Nat.instMonoid` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Int.instMonoid` `Nat.totient`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `IsCyclotomicExtension.zeta_spec` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `RingHom.injective_int` `Rat.instCharZero` `NumberField.discr_eq_discr` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `Algebra.discr_localizationLocalization` `instIsDomain` `PowerBasis.finrank` `commRing_strongRankCondition` `Int.instNontrivial` `Rat.nontrivial` `NumberField.RingOfIntegers.rank` `Algebra.discr_reindex` `Module.Basis.localizationLocalization_apply` `PowerBasis.coe_basis` `IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen` `PowerBasis.basis_eq_pow` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `map_natCast` `IsCyclotomicExtension.discr_prime_pow` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos`
`discr_prime_pow'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Algebra.discr` `PowerBasis.dim` `Rat.instField` `CommRing.toRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `IsPrimitiveRoot.subOnePowerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Rat.commRing` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Module.Basis.instFunLike` `PowerBasis.basis` `Nat.totient`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `IsCyclotomicExtension.discr_prime_pow` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one`
`discr_prime_pow_eq_unit_mul_pow'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Algebra.discr` `PowerBasis.dim` `Rat.instField` `CommRing.toRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `IsPrimitiveRoot.subOnePowerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Rat.commRing` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Module.Basis.instFunLike` `PowerBasis.basis` `Units.val` `Int.instMonoid`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one` `IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos`
`discr_prime_pow_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Algebra.discr` `PowerBasis.dim` `Rat.instField` `CommRing.toRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `IsPrimitiveRoot.subOnePowerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Rat.commRing` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Module.Basis.instFunLike` `PowerBasis.basis` `Nat.totient`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `IsCyclotomicExtension.discr_prime_pow_ne_two` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one`
`discr_prime_pow_succ` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `Nat.instMonoid` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Int.instMonoid`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Nat.totient_prime_pow` `Fact.out` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `discr_prime_pow`
`finrank` 📖	mathematical	—	`Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Nat.totient`	—	`IsCyclotomicExtension.finrank` `instIsDomain` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `Nat.instCanonicallyOrderedAdd`
`isIntegralClosure_adjoin_singleton` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsIntegralClosure` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Int.instCommRing` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id`	—	`FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `instFaithfulSMul_1` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AddCommGroup.intIsScalarTower` `adjoin_singleton_eq_top` `IsIntegralClosure.isIntegral_iff` `NumberField.RingOfIntegers.instIsIntegralClosureInt` `AlgHom.map_adjoin_singleton` `Algebra.map_top`
`isIntegralClosure_adjoin_singleton_of_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsIntegralClosure` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Int.instCommRing` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id`	—	`isIntegralClosure_adjoin_singleton_of_prime_pow` `pow_one`
`isIntegralClosure_adjoin_singleton_of_prime_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`IsIntegralClosure` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Int.instCommRing` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id`	—	`Subtype.val_injective` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `IsIntegral.sub` `IsPrimitiveRoot.isIntegral` `NeZero.pos` `isIntegral_one` `Algebra.discr_mul_isIntegral_mem_adjoin` `IsCyclotomicExtension.finiteDimensional` `Finite.of_fintype` `AddCommGroup.intIsScalarTower` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `PerfectField.ofCharZero` `Rat.instCharZero` `IsDedekindDomainDvr.isIntegrallyClosed` `Int.instIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Rat.isFractionRing` `discr_prime_pow_eq_unit_mul_pow'` `Subalgebra.smul_mem` `IsCyclotomicExtension.singleton_one` `pow_zero` `Algebra.mem_top` `Algebra.mem_bot` `isIntegral_algebraMap_iff` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegrallyClosed.isIntegral_iff` `IsScalarTower.algebraMap_apply` `Subalgebra.algebraMap_mem` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.smul_def` `one_mul` `Int.cast_one` `Units.inv_mul` `Int.cast_mul` `zsmul_eq_mul` `Units.inv_eq_val_inv` `smul_mul_assoc` `IsScalarTower.right` `smul_assoc` `minpoly.isIntegrallyClosed_eq_field_fractions'` `IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp` `Polynomial.cyclotomic.irreducible_rat` `IsPrimitiveRoot.subOnePowerBasis_gen` `Polynomial.map_injective` `RingHom.injective_int` `Polynomial.map_comp` `Polynomial.map_add` `Polynomial.map_X` `Polynomial.map_one` `Polynomial.map_cyclotomic_int` `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt` `Algebra.adjoin_le` `Subalgebra.sub_mem` `Algebra.self_mem_adjoin_singleton` `Subalgebra.one_mem` `mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt` `Nat.prime_iff_prime_int` `Fact.out` `Int.cast_pow` `Int.cast_natCast` `map_natCast` `IsIntegral.algebraMap` `Algebra.IsIntegral.isIntegral` `le_integralClosure_iff_isIntegral` `adjoin_le_integralClosure`
`natAbs_discr` 📖	mathematical	—	`NumberField.discr` `IsCyclotomicExtension.numberField` `Set` `Set.instSingletonSet` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `Rat.numberField` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `Monoid.toNatPow` `Nat.instMonoid` `Nat.totient` `Finset.prod` `Nat.instCommMonoid` `Nat.primeFactors`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `discr` `one_pow` `one_mul` `Nat.cast_pow` `Nat.prod_primeFactors_pow_totient_ediv_dvd` `NeZero.pos` `Nat.instCanonicallyOrderedAdd`
`torsionOrder_eq` 📖	mathematical	—	`NumberField.Units.torsionOrder` `Even` `Nat.instDecidablePredEven`	—	`NumberField.to_charZero` `IsCyclotomicExtension.zeta_spec` `NumberField.Units.torsionOrder.eq_1` `Fintype.card_eq_nat_card` `IsCyclic.exists_ofOrder_eq_natCard` `NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion` `IsPrimitiveRoot.map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsPrimitiveRoot.coe_units_iff` `IsPrimitiveRoot.coe_submonoidClass_iff` `IsPrimitiveRoot.iff_orderOf` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NumberField.RingOfIntegers.instIsTorsionFree_2` `IsPrimitiveRoot.pow_mul_pow_lcm` `NumberField.Units.torsionOrder_ne_zero` `NeZero.of_pos` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `NumberField.Units.torsionOrder_pos` `IsCyclotomicExtension.union_of_isPrimitiveRoot` `IsCyclotomicExtension.iff_union_of_dvd` `Set.union_comm` `finrank` `Nat.even_or_odd` `dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Even.eq_of_totient_eq_totient` `NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot` `Nat.not_even_iff_odd` `Nat.eq_or_eq_of_totient_eq_totient` `Odd.of_dvd_nat` `NumberField.Units.even_torsionOrder`

IsPrimitiveRoot

Definitions

Name	Category	Theorems
`adjoinEquivRingOfIntegers` 📖	CompOp	2 math math: `adjoinEquivRingOfIntegers_symm_apply`, `adjoinEquivRingOfIntegers_apply`
`adjoinEquivRingOfIntegersOfPrimePow` 📖	CompOp	2 math math: `adjoinEquivRingOfIntegersOfPrimePow_apply`, `adjoinEquivRingOfIntegersOfPrimePow_symm_apply`
`integralPowerBasis` 📖	CompOp	4 math math: `integralPowerBasis'_gen`, `power_basis_int'_dim`, `integralPowerBasis_dim`, `integralPowerBasis_gen`
`integralPowerBasis'` 📖	CompOp	—
`integralPowerBasisOfPrimePow` 📖	CompOp	2 math math: `integralPowerBasisOfPrimePow_gen`, `integralPowerBasisOfPrimePow_dim`
`subOneIntegralPowerBasis` 📖	CompOp	4 math math: `subOneIntegralPowerBasis_gen_prime`, `subOneIntegralPowerBasis_gen`, `subOneIntegralPowerBasis'_gen_prime`, `subOneIntegralPowerBasis'_gen`
`subOneIntegralPowerBasis'` 📖	CompOp	—
`subOneIntegralPowerBasisOfPrimePow` 📖	CompOp	2 math math: `subOneIntegralPowerBasisOfPrimePow_gen`, `subOneIntegralPowerBasisOfPrimePow_gen_prime`
`toInteger` 📖	CompOp	68 math math: `toInteger_isPrimitiveRoot`, `IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one`, `not_exists_int_prime_dvd_sub_of_prime_ne_two'`, `zeta_sub_one_prime_of_two_pow`, `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b`, `norm_toInteger_sub_one_of_eq_two_pow`, `zeta_sub_one_prime_of_ne_two`, `IsCyclotomicExtension.Rat.Three.coe_eta`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one'`, `FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube`, `FermatLastTheoremForThreeGen.Solution.hab`, `FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b`, `norm_toInteger_sub_one_of_eq_two`, `not_exists_int_prime_dvd_sub_of_prime_ne_two`, `integralPowerBasisOfPrimePow_gen`, `prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one`, `norm_toInteger_pow_sub_one_of_two`, `integralPowerBasis'_gen`, `prime_norm_toInteger_sub_one_of_prime_ne_two'`, `FermatLastTheoremForThreeGen.Solution'.ha`, `finite_quotient_span_sub_one'`, `finite_quotient_span_sub_one`, `FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one`, `IsCyclotomicExtension.Rat.Three.eta_sq`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one`, `finite_quotient_toInteger_sub_one`, `norm_toInteger_sub_one_eq_one`, `IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'`, `IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one'`, `IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one`, `IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver`, `IsCyclotomicExtension.Rat.Three.Units.mem`, `IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one`, `prime_norm_toInteger_sub_one_of_prime_ne_two`, `FermatLastTheoremForThreeGen.Solution'.hcdvd`, `toInteger_sub_one_dvd_prime`, `norm_toInteger_sub_one_of_prime_ne_two`, `toInteger_sub_one_dvd_prime'`, `FermatLastTheoremForThreeGen.Solution'.hb`, `card_quotient_toInteger_sub_one`, `IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one`, `not_exists_int_prime_dvd_sub_of_prime_pow_ne_two`, `norm_toInteger_pow_sub_one_of_prime_pow_ne_two`, `IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow`, `IsCyclotomicExtension.Rat.adjoin_singleton_eq_top`, `coe_toInteger`, `integralPowerBasis_gen`, `IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one`, `IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one`, `zeta_sub_one_prime`, `FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul`, `IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul`, `FermatLastTheoremForThreeGen.lambda_sq_dvd_c`, `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b`, `norm_toInteger_sub_one_of_prime_ne_two'`, `FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite`, `FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one`, `norm_toInteger_pow_sub_one_of_prime_ne_two`, `toInteger_cube_eq_one`, `zeta_sub_one_prime'`, `toInteger_sub_one_not_dvd_two`, `IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one`, `FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoinEquivRingOfIntegersOfPrimePow_apply` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `AlgEquiv` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `NumberField.RingOfIntegers` `Subalgebra.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subalgebra.algebra` `CommRing.toRing` `AlgEquiv.instFunLike` `adjoinEquivRingOfIntegersOfPrimePow` `AlgHom` `Int.instCommRing` `Polynomial.instCommRingAdjoinSingleton` `AlgHom.funLike` `IsIntegralClosure.lift` `NumberField.RingOfIntegers.instAlgebra_1` `Algebra.id` `Semifield.toCommSemiring` `NumberField.RingOfIntegers.instIsIntegralClosureInt` `Subalgebra.toAlgebra` `IsIntegralClosure.isIntegral_algebra` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`	—	—
`adjoinEquivRingOfIntegersOfPrimePow_symm_apply` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `AlgEquiv` `NumberField.RingOfIntegers` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subalgebra.toSemiring` `CommRing.toRing` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `adjoinEquivRingOfIntegersOfPrimePow` `AlgHom` `Int.instCommRing` `Polynomial.instCommRingAdjoinSingleton` `AlgHom.funLike` `IsIntegralClosure.lift` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `Algebra.id` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow` `NumberField.RingOfIntegers.instAlgebra_1` `IsIntegralClosure.isIntegral_algebra` `NumberField.RingOfIntegers.instIsIntegralClosureInt`	—	—
`adjoinEquivRingOfIntegers_apply` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `AlgEquiv` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `NumberField.RingOfIntegers` `Subalgebra.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subalgebra.algebra` `CommRing.toRing` `AlgEquiv.instFunLike` `adjoinEquivRingOfIntegers` `AlgHom` `Int.instCommRing` `Polynomial.instCommRingAdjoinSingleton` `AlgHom.funLike` `IsIntegralClosure.lift` `NumberField.RingOfIntegers.instAlgebra_1` `Algebra.id` `Semifield.toCommSemiring` `NumberField.RingOfIntegers.instIsIntegralClosureInt` `Subalgebra.toAlgebra` `IsIntegralClosure.isIntegral_algebra` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton`	—	—
`adjoinEquivRingOfIntegers_symm_apply` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `AlgEquiv` `NumberField.RingOfIntegers` `Subalgebra` `Int.instCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subalgebra.toSemiring` `CommRing.toRing` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `adjoinEquivRingOfIntegers` `AlgHom` `Int.instCommRing` `Polynomial.instCommRingAdjoinSingleton` `AlgHom.funLike` `IsIntegralClosure.lift` `Subalgebra.toAlgebra` `Semifield.toCommSemiring` `Algebra.id` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton` `NumberField.RingOfIntegers.instAlgebra_1` `IsIntegralClosure.isIntegral_algebra` `NumberField.RingOfIntegers.instIsIntegralClosureInt`	—	—
`card_quotient_toInteger_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Nat.card` `HasQuotient.Quotient` `NumberField.RingOfIntegers` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra`	—	`Submodule.cardQuot_apply` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Ideal.absNorm_apply` `Ideal.absNorm_span_singleton` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt`
`coe_toInteger` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Subalgebra` `CommRing.toCommSemiring` `Int.instCommRing` `CommSemiring.toSemiring` `Ring.toIntAlgebra` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `toInteger`	—	—
`finite_quotient_span_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Finite` `HasQuotient.Quotient` `NumberField.RingOfIntegers` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Ideal.finiteQuotientOfFreeOfNeBot` `NumberField.RingOfIntegers.instIsDomain` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `ne_one` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_lt` `Fact.out` `NumberField.RingOfIntegers.ext_iff`
`finite_quotient_span_sub_one'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Finite` `HasQuotient.Quotient` `NumberField.RingOfIntegers` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`zero_add` `pow_one` `finite_quotient_span_sub_one`
`finite_quotient_toInteger_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Finite` `HasQuotient.Quotient` `NumberField.RingOfIntegers` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Ideal.finiteQuotientOfFreeOfNeBot` `NumberField.RingOfIntegers.instIsDomain` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `NeZero.of_gt` `Nat.instCanonicallyOrderedAdd` `ne_one` `NumberField.RingOfIntegers.ext_iff`
`integralPowerBasis'_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasis` `toInteger`	—	`integralPowerBasis_gen`
`integralPowerBasisOfPrimePow_dim` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`PowerBasis.dim` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasisOfPrimePow` `Nat.totient`	—	`Polynomial.cyclotomic_eq_minpoly` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.Prime.one_lt'` `Polynomial.natDegree_cyclotomic` `Int.instNontrivial`
`integralPowerBasisOfPrimePow_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasisOfPrimePow` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Int.instIsDomain` `integralPowerBasisOfPrimePow.eq_1` `PowerBasis.map_gen` `SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin.powerBasis'_gen` `IsIntegralClosure.algebraMap_lift` `NumberField.RingOfIntegers.instIsIntegralClosureInt` `IsIntegralClosure.isIntegral_algebra` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`
`integralPowerBasis_dim` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.dim` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasis` `Nat.totient`	—	`Polynomial.cyclotomic_eq_minpoly` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Polynomial.natDegree_cyclotomic` `Int.instNontrivial`
`integralPowerBasis_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasis` `toInteger`	—	`Int.instIsDomain` `integralPowerBasis.eq_1` `PowerBasis.map_gen` `SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin.powerBasis'_gen` `IsIntegralClosure.algebraMap_lift` `NumberField.RingOfIntegers.instIsIntegralClosureInt` `IsIntegralClosure.isIntegral_algebra` `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton`
`norm_toInteger_pow_sub_one_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Int.instMonoid`	—	`norm_toInteger_pow_sub_one_of_prime_pow_ne_two` `eq_of_prime_pow_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.Prime.prime` `Fact.out` `Nat.prime_two` `pow_one`
`norm_toInteger_pow_sub_one_of_prime_pow_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Int.instMonoid`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Algebra.norm_eq_iff` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `le_rfl` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_one` `MonoidHomClass.toOneHomClass` `norm_pow_sub_one_of_prime_pow_ne_two` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `eq_intCast` `Int.cast_pow` `Int.cast_natCast`
`norm_toInteger_pow_sub_one_of_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Int.instMonoid`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Algebra.norm_eq_iff` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `le_rfl` `Nat.instAtLeastTwoHAddOfNat` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_one` `MonoidHomClass.toOneHomClass` `norm_pow_sub_one_two` `Polynomial.cyclotomic.irreducible_rat` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `eq_intCast` `Int.cast_pow` `Int.cast_neg` `Int.cast_ofNat`
`norm_toInteger_sub_one_eq_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `NeZero.of_gt` `Nat.instCanonicallyOrderedAdd` `Algebra.norm_eq_iff` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `le_rfl` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `sub_one_norm_eq_eval_cyclotomic` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `Polynomial.eval_one_cyclotomic_not_prime_pow` `Int.cast_one`
`norm_toInteger_sub_one_of_eq_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.natPow_one` `zero_add` `pow_one` `toInteger.congr_simp` `pow_zero` `norm_toInteger_pow_sub_one_of_two`
`norm_toInteger_sub_one_of_eq_two_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Algebra.norm_eq_iff` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `le_rfl` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `eq_intCast` `Nat.instAtLeastTwoHAddOfNat` `Int.cast_ofNat` `norm_sub_one_two` `Polynomial.cyclotomic.irreducible_rat`
`norm_toInteger_sub_one_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `pow_zero` `pow_one` `norm_toInteger_pow_sub_one_of_prime_ne_two`
`norm_toInteger_sub_one_of_prime_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`zero_add` `pow_one` `norm_toInteger_sub_one_of_prime_ne_two`
`not_exists_int_prime_dvd_sub_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddGroupWithOne.toIntCast`	—	`not_exists_int_prime_dvd_sub_of_prime_pow_ne_two` `Nat.Prime.pow_eq_iff` `Nat.prime_two` `pow_one`
`not_exists_int_prime_dvd_sub_of_prime_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddGroupWithOne.toIntCast`	—	`zero_add` `pow_one` `not_exists_int_prime_dvd_sub_of_prime_ne_two`
`not_exists_int_prime_dvd_sub_of_prime_pow_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddGroupWithOne.toIntCast`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `integralPowerBasisOfPrimePow_dim` `Nat.totient_prime_pow` `Fact.out` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.Prime.one_lt` `ne_of_gt` `pow_zero` `one_mul` `Ne.lt_of_le` `zero_add` `pow_one` `Nat.Prime.two_le` `one_lt_mul_of_lt_of_le` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `one_lt_pow₀` `RingHomInvPair.ids` `Module.Basis.ext_elem_iff` `sub_eq_iff_eq_add` `PowerBasis.basis_eq_pow` `Prime.not_dvd_one` `Int.prime_iff_natAbs_prime` `MulZeroClass.mul_zero` `add_zero` `Module.Basis.repr_self_apply` `Module.Basis.coord_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `zsmul_one` `zsmul_eq_mul` `Int.cast_natCast` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `PowerBasis.coe_basis` `integralPowerBasisOfPrimePow_gen`
`power_basis_int'_dim` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.dim` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `integralPowerBasis` `Nat.totient`	—	`integralPowerBasis_dim`
`prime_dvd_of_dvd_norm_sub_one` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—	`NeZero.of_gt` `Nat.instCanonicallyOrderedAdd` `NumberField.to_charZero` `IntermediateField.charZero` `Rat.instCharZero` `intermediateField_adjoin_isCyclotomicExtension` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `NumberField.to_finiteDimensional` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `coe_submonoidClass_iff` `NumberField.of_intermediateField` `Rat.numberField` `Algebra.norm_eq_iff` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `le_rfl` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `SubringClass.addSubgroupClass` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Algebra.norm_norm` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Rat.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsScalarTower.rat` `instIsDomain` `IntermediateField.finiteDimensional_right` `Algebra.norm_algebraMap` `map_pow` `MonoidHom.instMonoidHomClass` `Algebra.norm_localization` `lt_or_eq_of_le` `pow_zero` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.false` `pow_one` `zero_add` `norm_toInteger_sub_one_of_eq_two_pow` `NeZero.of_gt'` `Nat.Prime.one_lt'` `norm_toInteger_sub_one_of_prime_ne_two` `Nat.Prime.ne_one` `Fact.out` `Int.natCast_dvd_ofNat` `one_pow` `norm_toInteger_sub_one_eq_one` `Mathlib.Tactic.Push.not_and_eq` `Nat.prime_two` `one_ne_zero` `IsUnit.dvd_mul_left` `isUnit_pow_iff` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isUnit_neg_one` `mul_pow` `neg_eq_neg_one_mul` `norm_toInteger_sub_one_of_eq_two` `Nat.prime_dvd_prime_iff_eq` `Nat.Prime.dvd_of_dvd_pow` `dvd_pow_self`
`prime_norm_toInteger_sub_one_of_prime_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `norm_toInteger_sub_one_of_prime_ne_two` `Nat.prime_iff_prime_int` `Fact.out`
`prime_norm_toInteger_sub_one_of_prime_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`zero_add` `pow_one` `prime_norm_toInteger_sub_one_of_prime_ne_two`
`prime_norm_toInteger_sub_one_of_prime_pow_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `DFunLike.coe` `MonoidHom` `NumberField.RingOfIntegers` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `MonoidHom.instFunLike` `Algebra.norm` `Ring.toIntAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `norm_toInteger_pow_sub_one_of_prime_pow_ne_two` `zero_le` `pow_zero` `pow_one` `Nat.prime_iff_prime_int` `Fact.out`
`subOneIntegralPowerBasis'_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasis` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Subalgebra.one_mem`	—	`subOneIntegralPowerBasis_gen`
`subOneIntegralPowerBasis'_gen_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasis` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Subalgebra.one_mem`	—	`subOneIntegralPowerBasis_gen`
`subOneIntegralPowerBasisOfPrimePow_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasisOfPrimePow` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.instPreorder` `Nat.instOne` `Nat.Prime.one_lt'` `Subalgebra.one_mem`	—	`Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.Prime.one_lt'` `Subalgebra.one_mem` `PowerBasis.ofAdjoinEqTop'_gen` `Int.instIsDomain` `NumberField.RingOfIntegers.instIsDomain`
`subOneIntegralPowerBasisOfPrimePow_gen_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `PowerBasis.gen` `Int.instCommRing` `CommRing.toRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasisOfPrimePow`	—	`Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.Prime.one_lt'` `Subalgebra.one_mem` `subOneIntegralPowerBasisOfPrimePow_gen` `zeta_sub_one_prime`
`subOneIntegralPowerBasis_gen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasis` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Subalgebra.one_mem`	—	`Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `Subalgebra.one_mem` `PowerBasis.ofAdjoinEqTop'_gen` `Int.instIsDomain` `NumberField.RingOfIntegers.instIsDomain`
`subOneIntegralPowerBasis_gen_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`PowerBasis.gen` `NumberField.RingOfIntegers` `Int.instCommRing` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `subOneIntegralPowerBasis` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Subalgebra.sub_mem` `isIntegral` `NeZero.pos` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Subalgebra.one_mem`	—	`subOneIntegralPowerBasis_gen`
`toInteger_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `NumberField.RingOfIntegers.instCommRing` `toInteger`	—	`of_map_of_injective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NumberField.RingOfIntegers.coe_injective`
`toInteger_sub_one_dvd_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.Prime.pow_eq_iff` `Nat.prime_two` `eq_neg_one_of_two_right` `IsDomain.to_noZeroDivisors` `instIsDomain` `pow_one` `zero_add` `AddRightCancelSemigroup.toIsRightCancelAdd` `NumberField.RingOfIntegers.ext` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `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.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `norm_toInteger_pow_sub_one_of_prime_pow_ne_two` `zero_le` `Ideal.norm_dvd_iff` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `prime_norm_toInteger_sub_one_of_prime_pow_ne_two` `pow_zero` `Int.cast_natCast`
`toInteger_sub_one_dvd_prime'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`zero_add` `pow_one` `toInteger_sub_one_dvd_prime`
`toInteger_sub_one_not_dvd_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.instAtLeastTwoHAddOfNat` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Int.cast_ofNat` `prime_dvd_prime_iff_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.prime_iff` `Fact.out` `Nat.prime_two` `norm_toInteger_sub_one_of_prime_ne_two` `Ideal.norm_dvd_iff` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `Nat.prime_iff_prime_int`
`zeta_sub_one_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `zeta_sub_one_prime_of_two_pow` `zeta_sub_one_prime_of_ne_two`
`zeta_sub_one_prime'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `zero_add` `pow_one` `zeta_sub_one_prime`
`zeta_sub_one_prime_of_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Ideal.prime_of_irreducible_absNorm_span` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `NumberField.RingOfIntegers.instFreeInt` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `pow_ne_one_of_pos_of_lt` `one_ne_zero` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_lt` `Fact.out` `pow_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `Nat.irreducible_iff_prime` `Ideal.absNorm_span_singleton` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `Nat.prime_iff` `Int.prime_iff_natAbs_prime` `RingHom.injective_int` `Rat.instCharZero` `Algebra.norm_localization` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `map_natCast` `norm_sub_one_of_prime_ne_two` `Polynomial.cyclotomic.irreducible_rat` `NeZero.pos` `Nat.prime_iff_prime_int`
`zeta_sub_one_prime_of_two_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid`	`Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `Ideal.prime_of_irreducible_absNorm_span` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `pow_ne_one_of_pos_of_lt` `one_ne_zero` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `pow_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `Nat.irreducible_iff_prime` `Ideal.absNorm_span_singleton` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `Nat.prime_iff` `Int.prime_iff_natAbs_prime` `RingHom.injective_int` `Rat.instCharZero` `Algebra.norm_localization` `Rat.isFractionRing` `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `AddCommGroup.intIsScalarTower` `Nat.instAtLeastTwoHAddOfNat` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_ofNat` `zero_add` `toInteger.congr_simp` `pow_zero` `norm_pow_sub_one_two` `Polynomial.cyclotomic.irreducible_rat` `Nat.instNontrivial` `Prime.neg` `Int.prime_two` `algebraMap_int_eq` `norm_sub_one_two` `Nat.AtLeastTwo.prop` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono`

IsPrimitiveRoot.IsCyclotomicExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ringOfIntegersOfPrimePow` 📖	mathematical	—	`IsCyclotomicExtension` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `Nat.instMonoid` `NumberField.RingOfIntegers` `Int.instCommRing` `NumberField.RingOfIntegers.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `IsPrimitiveRoot.adjoin_isCyclotomicExtension` `IsCyclotomicExtension.zeta_spec` `IsCyclotomicExtension.equiv`

NumberField.Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_torsionOrder_of_isPrimitiveRoot` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`torsionOrder`	—	`torsionOrder.eq_1` `Fintype.card_eq_nat_card` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `IsPrimitiveRoot.isUnit_unit` `CommGroup.mem_torsion` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `isPeriodicPt_mul_iff_pow_eq_one` `IsPrimitiveRoot.pow_eq_one` `IsPrimitiveRoot.eq_orderOf` `orderOf_dvd_natCard`

---

← Back to Index