PrimitiveRoots

📁 Source: Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Statistics

Metric	Count
Definitions `IsPrimitiveRoot`, `autToPow`, `primitiveRootsPowEquiv`, `primitiveRootsPowEquivOfCoprime`, `toRootsOfUnity`, `zmodEquivZPowers`, `primitiveRoots`, `rootsOfUnityEquivOfPrimitiveRoots`	8
Theorems `exists_apply_ne_one`, `adjoin_pair_eq`, `autToPow_spec`, `card_nthRoots`, `card_nthRootsFinset`, `card_nthRoots_one`, `card_primitiveRoots`, `card_rootsOfUnity`, `card_rootsOfUnity'`, `coe_autToPow_apply`, `coe_submonoidClass_iff`, `coe_units_iff`, `disjoint`, `dvd_of_pow_eq_one`, `eq_neg_one_of_two_right`, `eq_orderOf`, `eq_pow_of_mem_rootsOfUnity`, `eq_pow_of_pow_eq_one`, `existsUnique`, `exists_pos`, `geom_sum_eq_zero`, `iff`, `iff_def`, `iff_orderOf`, `injOn_pow`, `injOn_pow_mul`, `inv`, `inv_iff`, `isOfFinOrder`, `isPrimitiveRoot_iff`, `isPrimitiveRoot_iff'`, `isUnit`, `isUnit_unit`, `isUnit_unit'`, `map_iff_of_injective`, `map_of_injective`, `map_rootsOfUnity`, `mem_nthRootsFinset`, `mem_rootsOfUnity`, `mk_of_lt`, `neZero'`, `ne_one`, `ne_zero`, `neg_one`, `not_iff`, `nthRoots_eq`, `nthRoots_nodup`, `nthRoots_one_eq_biUnion_primitiveRoots`, `nthRoots_one_nodup`, `of_map_of_injective`, `of_subsingleton`, `one`, `one_right_iff`, `orderOf`, `pow`, `pow_eq_one`, `pow_eq_one_iff_dvd`, `pow_iff_coprime`, `pow_inj`, `pow_mul_pow_lcm`, `pow_ne_one_of_pos_of_lt`, `pow_of_coprime`, `pow_of_dvd`, `pow_of_prime`, `pow_sub_one_eq`, `primitiveRootsPowEquivOfCoprime_apply_coe`, `primitiveRootsPowEquiv_apply_coe`, `primitiveRootsPowEquiv_symm_apply_coe`, `primitiveRoots_one`, `sub_one_ne_zero`, `unique`, `val_inv_toRootsOfUnity_coe`, `val_toRootsOfUnity_coe`, `zero`, `zmodEquivZPowers_apply_coe_int`, `zmodEquivZPowers_apply_coe_nat`, `zmodEquivZPowers_symm_apply_pow`, `zmodEquivZPowers_symm_apply_pow'`, `zmodEquivZPowers_symm_apply_zpow`, `zmodEquivZPowers_symm_apply_zpow'`, `zpow_eq_one`, `zpow_eq_one_iff_dvd`, `zpow_of_gcd_eq_one`, `zpowers_eq`, `exists_monoidHom_apply_ne_one`, `card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot`, `isPrimitiveRoot_of_mem_primitiveRoots`, `isPrimitiveRoot_of_mem_rootsOfUnity`, `mem_primitiveRoots`, `primitiveRoots_zero`, `rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val`, `rootsOfUnityEquivOfPrimitiveRoots_symm_apply`, `val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe`	93
Total	101

IsCyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_apply_ne_one` 📖	—	`IsPrimitiveRoot` `CommGroup.toCommMonoid` `Nat.card`	—	—	`exists_generator` `IsPrimitiveRoot.eq_orderOf` `orderOf_eq_card_of_forall_mem_zpowers` `Nat.card_eq_fintype_card` `dvd_refl` `monoidHomOfForallMemZpowers_apply_gen` `Mathlib.Tactic.Contrapose.contrapose₄` `Submonoid.mem_powers_iff` `mem_powers_iff_mem_zpowers` `IsPrimitiveRoot.pow_eq_one_iff_dvd` `map_pow` `MonoidHom.instMonoidHomClass` `pow_mul` `pow_card_eq_one` `one_pow`

IsPrimitiveRoot

Definitions

Name	Category	Theorems
`autToPow` 📖	CompOp	5 math math: `autToPow_eq_modularCyclotomicCharacter`, `coe_autToPow_apply`, `autToPow_injective`, `autToPow_spec`, `IsCyclotomicExtension.autEquivPow_apply`
`primitiveRootsPowEquiv` 📖	CompOp	2 math math: `primitiveRootsPowEquiv_symm_apply_coe`, `primitiveRootsPowEquiv_apply_coe`
`primitiveRootsPowEquivOfCoprime` 📖	CompOp	1 math math: `primitiveRootsPowEquivOfCoprime_apply_coe`
`toRootsOfUnity` 📖	CompOp	3 math math: `val_toRootsOfUnity_coe`, `coe_autToPow_apply`, `val_inv_toRootsOfUnity_coe`
`zmodEquivZPowers` 📖	CompOp	6 math math: `zmodEquivZPowers_symm_apply_pow'`, `zmodEquivZPowers_symm_apply_pow`, `zmodEquivZPowers_symm_apply_zpow'`, `zmodEquivZPowers_apply_coe_nat`, `zmodEquivZPowers_apply_coe_int`, `zmodEquivZPowers_symm_apply_zpow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_pair_eq` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Algebra.adjoin` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`le_antisymm` `Algebra.adjoin_le` `Set.pair_subset_iff` `eq_pow_of_pow_eq_one` `pow_eq_one_iff_dvd` `Subalgebra.pow_mem` `Algebra.self_mem_adjoin_singleton` `pow_mul_pow_lcm` `pow_eq_one` `pow_mem` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Algebra.mem_adjoin_of_mem`
`autToPow_spec` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.val` `Units.val` `ZMod` `ZMod.commRing` `DFunLike.coe` `MonoidHom` `AlgEquiv` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMulOneClass` `MonoidHom.instFunLike` `autToPow` `AlgEquiv.instFunLike`	—	`map_rootsOfUnity_eq_pow_self` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `coe_autToPow_apply` `rootsOfUnity.coe_pow` `pow_eq_pow_iff_modEq` `ZMod.val_natCast` `eq_orderOf` `Subgroup.orderOf_coe` `orderOf_units` `Nat.mod_modEq`
`card_nthRoots` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Multiset.card` `Polynomial.nthRoots` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`nthRoots_eq` `Multiset.card_map` `Multiset.card_range` `Polynomial.nthRoots_zero` `Polynomial.mem_nthRoots`
`card_nthRootsFinset` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Finset.card` `Polynomial.nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Polynomial.nthRootsFinset.eq_1` `nthRoots_one_nodup` `Multiset.toFinset_eq` `card_nthRoots_one`
`card_nthRoots_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Multiset.card` `Polynomial.nthRoots` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`card_nthRoots` `pow_eq_one`
`card_primitiveRoots` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Finset.card` `primitiveRoots` `Nat.totient`	—	`primitiveRoots.congr_simp` `primitiveRoots_zero` `Finset.card_bij` `mem_primitiveRoots` `pow_of_coprime` `isPrimitiveRoot_iff`
`card_rootsOfUnity` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Fintype.card` `Units` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `rootsOfUnity.fintype`	—	`isUnit` `card_rootsOfUnity'` `coe_units_iff`
`card_rootsOfUnity'` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`Fintype.card` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `rootsOfUnity.fintype`	—	`Fintype.card_congr` `zpowers_eq` `ZMod.card`
`coe_autToPow_apply` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Units.val` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `DFunLike.coe` `MonoidHom` `AlgEquiv` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMulOneClass` `MonoidHom.instFunLike` `autToPow` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AlgEquiv.instFunLike` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `toRootsOfUnity` `Monoid.toNatPow` `map_rootsOfUnity_eq_pow_self` `MonoidWithZeroHomClass.toMonoidHomClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass`	—	—
`coe_submonoidClass_iff` 📖	mathematical	—	`IsPrimitiveRoot` `SetLike.instMembership` `SubmonoidClass.toCommMonoid`	—	`SubmonoidClass.toOneMemClass`
`coe_units_iff` 📖	mathematical	—	`IsPrimitiveRoot` `Units.val` `CommMonoid.toMonoid` `Units` `CommGroup.toCommMonoid` `Units.instCommGroupUnits`	—	—
`disjoint` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `primitiveRoots`	—	`Finset.disjoint_left` `unique` `isPrimitiveRoot_of_mem_primitiveRoots`
`dvd_of_pow_eq_one` 📖	—	`IsPrimitiveRoot` `Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	—
`eq_neg_one_of_two_right` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sq_eq_one_iff` `pow_eq_one` `ne_one` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`eq_orderOf` 📖	mathematical	`IsPrimitiveRoot`	`orderOf` `CommMonoid.toMonoid`	—	`unique` `orderOf`
`eq_pow_of_mem_rootsOfUnity` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `Subgroup` `CommMonoid.toMonoid` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity`	`Monoid.toNatPow` `Units.instMonoid`	—	`zpowers_eq` `Nat.cast_zero` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `ne_of_gt` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `zpow_add` `zpow_mul` `zpow_eq_one` `one_zpow` `mul_one`
`eq_pow_of_pow_eq_one` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `isUnit` `IsUnit.of_pow_eq_one` `eq_pow_of_mem_rootsOfUnity` `coe_units_iff` `mem_rootsOfUnity'`
`existsUnique` 📖	mathematical	—	`ExistsUnique` `IsPrimitiveRoot`	—	`orderOf` `unique`
`exists_pos` 📖	mathematical	`Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsPrimitiveRoot`	—	`orderOf_pos_iff` `isOfFinOrder_iff_pow_eq_one` `orderOf`
`geom_sum_eq_zero` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eq_zero_of_ne_zero_of_mul_left_eq_zero` `IsDomain.to_noZeroDivisors` `sub_ne_zero_of_ne` `ne_one` `mul_neg_geom_sum` `pow_eq_one` `sub_self`
`iff` 📖	mathematical	—	`IsPrimitiveRoot` `Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_eq_one` `pow_ne_one_of_lt_orderOf` `LT.lt.ne'` `eq_orderOf` `mk_of_lt`
`iff_def` 📖	mathematical	—	`IsPrimitiveRoot` `Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`iff_orderOf` 📖	mathematical	—	`IsPrimitiveRoot` `orderOf` `CommMonoid.toMonoid`	—	`not_iff_not` `not_iff`
`injOn_pow` 📖	mathematical	`IsPrimitiveRoot`	`Set.InjOn` `Monoid.toNatPow` `CommMonoid.toMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.range`	—	`Set.mem_Iio` `Finset.coe_range`
`injOn_pow_mul` 📖	mathematical	`IsPrimitiveRoot` `CommMonoidWithZero.toCommMonoid`	`Set.InjOn` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.range`	—	`injOn_pow` `IsCancelMulZero.toIsRightCancelMulZero`
`inv` 📖	mathematical	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`inv_pow` `pow_eq_one` `inv_one` `dvd_of_pow_eq_one`
`inv_iff` 📖	mathematical	—	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`inv` `inv_inv`
`isOfFinOrder` 📖	mathematical	`IsPrimitiveRoot`	`IsOfFinOrder` `CommMonoid.toMonoid`	—	`isPeriodicPt_mul_iff_pow_eq_one` `pow_eq_one`
`isPrimitiveRoot_iff` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`eq_pow_of_pow_eq_one` `pow_eq_one` `pow_iff_coprime` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `pow_of_coprime`
`isPrimitiveRoot_iff'` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`Monoid.toNatPow` `Units.instMonoid`	—	`eq_pow_of_mem_rootsOfUnity` `pow_eq_one` `pow_iff_coprime` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `pow_of_coprime`
`isUnit` 📖	mathematical	`IsPrimitiveRoot`	`IsUnit` `CommMonoid.toMonoid`	—	`IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `pow_succ'` `pow_eq_one`
`isUnit_unit` 📖	mathematical	`IsPrimitiveRoot`	`Units` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `IsUnit.unit` `isUnit`	—	`isUnit` `coe_units_iff`
`isUnit_unit'` 📖	mathematical	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid`	`Units` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `IsUnit.unit'` `isUnit`	—	`isUnit` `coe_units_iff`
`map_iff_of_injective` 📖	mathematical	`DFunLike.coe`	`IsPrimitiveRoot`	—	`of_map_of_injective` `map_of_injective`
`map_of_injective` 📖	—	`IsPrimitiveRoot` `DFunLike.coe`	—	—	`map_pow` `pow_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `eq_orderOf` `orderOf_dvd_of_pow_eq_one`
`map_rootsOfUnity` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `DFunLike.coe`	`Subgroup.map` `Units` `CommMonoid.toMonoid` `Units.instGroup` `Units.map` `MonoidHomClass.toMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `rootsOfUnity`	—	`isUnit` `isUnit_unit` `zpowers_eq` `map_of_injective` `MonoidHom.instMonoidHomClass` `Units.map_injective` `MonoidHom.map_zpowers`
`mem_nthRootsFinset` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Finset` `Finset.instMembership` `Polynomial.nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Polynomial.mem_nthRootsFinset` `pow_eq_one`
`mem_rootsOfUnity` 📖	mathematical	`IsPrimitiveRoot` `Units` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `Units.instCommGroupUnits`	`Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity`	—	`pow_eq_one`
`mk_of_lt` 📖	mathematical	`Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsPrimitiveRoot`	—	`LE.le.eq_of_not_lt`
`neZero'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`NeZero.of_not_dvd` `ringChar.charP` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `CharP.char_is_prime_of_pos` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `pow_ne_one_of_pos_of_lt` `lt_mul_of_one_lt_left` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_lt` `Fact.out` `isReduced_of_noZeroDivisors` `expChar_prime` `frobenius_def` `pow_mul'` `pow_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`ne_one` 📖	—	`IsPrimitiveRoot`	—	—	`pow_ne_one_of_pos_of_lt` `one_ne_zero` `pow_one`
`ne_zero` 📖	—	`IsPrimitiveRoot` `CommMonoidWithZero.toCommMonoid`	—	—	`unique` `zero`
`neg_one` 📖	mathematical	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`orderOf_neg_one` `ringChar.eq_iff` `orderOf`
`not_iff` 📖	mathematical	—	`IsPrimitiveRoot`	—	`orderOf` `unique`
`nthRoots_eq` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial.nthRoots` `Multiset.map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Multiset.range`	—	`Polynomial.nthRoots_zero` `Polynomial.nthRoots.congr_simp` `zero_pow` `LT.lt.ne'` `Polynomial.nthRoots_zero_right` `Multiset.map_congr` `MulZeroClass.mul_zero` `Multiset.map_const'` `Multiset.card_range` `Multiset.eq_of_le_of_card_le` `Finset.range_val` `Finset.image_val_of_injOn` `injOn_pow_mul` `IsDomain.toIsCancelMulZero` `Finset.val_le_iff_val_subset` `Polynomial.mem_nthRoots` `mul_pow` `pow_mul` `mul_comm` `pow_eq_one` `one_pow` `one_mul` `Multiset.card_map` `Polynomial.card_nthRoots`
`nthRoots_nodup` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Multiset.Nodup` `Polynomial.nthRoots`	—	`Polynomial.nthRoots_zero` `zero_pow` `LT.lt.ne'` `nthRoots_eq` `Multiset.nodup_map_iff_inj_on` `Multiset.nodup_range` `injOn_pow_mul` `IsDomain.toIsCancelMulZero` `Polynomial.mem_nthRoots`
`nthRoots_one_eq_biUnion_primitiveRoots` 📖	mathematical	—	`Polynomial.nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset.biUnion` `Nat.divisors` `primitiveRoots`	—	`Polynomial.nthRootsFinset.congr_simp` `Polynomial.nthRootsFinset_zero` `Nat.divisors_zero`
`nthRoots_one_nodup` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Multiset.Nodup` `Polynomial.nthRoots` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`nthRoots_nodup` `one_ne_zero` `NeZero.one` `IsDomain.toNontrivial`
`of_map_of_injective` 📖	—	`IsPrimitiveRoot` `DFunLike.coe`	—	—	`map_pow` `map_one` `MonoidHomClass.toOneHomClass` `pow_eq_one` `eq_orderOf` `orderOf_dvd_of_pow_eq_one`
`of_subsingleton` 📖	mathematical	—	`IsPrimitiveRoot`	—	`one_dvd`
`one` 📖	mathematical	—	`IsPrimitiveRoot` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`pow_one` `one_dvd`
`one_right_iff` 📖	mathematical	—	`IsPrimitiveRoot` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`pow_one` `pow_eq_one` `one`
`orderOf` 📖	mathematical	—	`IsPrimitiveRoot` `orderOf` `CommMonoid.toMonoid`	—	`pow_orderOf_eq_one` `orderOf_dvd_of_pow_eq_one`
`pow` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid`	—	`pow_eq_one` `dvd_of_pow_eq_one`
`pow_eq_one` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`pow_eq_one_iff_dvd` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`dvd_of_pow_eq_one` `pow_mul` `pow_eq_one` `one_pow`
`pow_iff_coprime` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid`	—	`mul_comm` `dvd_of_pow_eq_one` `pow_mul'` `mul_assoc` `pow_mul` `pow_eq_one` `one_pow` `LT.lt.ne'` `pow_of_coprime`
`pow_inj` 📖	—	`IsPrimitiveRoot` `Monoid.toNatPow` `CommMonoid.toMonoid`	—	—	`le_antisymm` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `dvd_of_pow_eq_one` `IsUnit.pow` `isUnit` `pow_add` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `one_mul` `lt_of_le_of_lt` `tsub_le_self` `le_of_not_ge`
`pow_mul_pow_lcm` 📖	mathematical	`IsPrimitiveRoot`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Monoid.toNatPow` `Nat.factorizationLCMLeft` `Nat.factorizationLCMRight`	—	`eq_orderOf` `Commute.orderOf_mul_pow_eq_lcm` `Commute.all` `orderOf`
`pow_ne_one_of_pos_of_lt` 📖	—	`IsPrimitiveRoot`	—	—	`dvd_of_pow_eq_one` `not_le_of_gt`
`pow_of_coprime` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid`	—	`pow_one` `isUnit` `Units.val_pow_eq_pow_val` `coe_units_iff` `pow_mul'` `pow_mul` `pow_eq_one` `one_pow` `dvd_of_pow_eq_one` `zpow_natCast` `Nat.gcd_eq_gcd_ab` `zpow_add` `mul_pow` `zpow_mul` `mul_right_comm` `one_zpow` `one_mul`
`pow_of_dvd` 📖	mathematical	`IsPrimitiveRoot`	`Monoid.toNatPow` `CommMonoid.toMonoid`	—	`eq_orderOf` `orderOf_pow_of_dvd` `orderOf`
`pow_of_prime` 📖	mathematical	`IsPrimitiveRoot` `Nat.Prime`	`Monoid.toNatPow` `CommMonoid.toMonoid`	—	`pow_of_coprime` `Nat.Prime.coprime_iff_not_dvd`
`pow_sub_one_eq` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range`	—	`eq_neg_iff_add_eq_zero` `add_comm` `Finset.sum_range_succ` `pos_of_gt` `Nat.instCanonicallyOrderedAdd` `geom_sum_eq_zero`
`primitiveRootsPowEquivOfCoprime_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `primitiveRoots` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `primitiveRootsPowEquivOfCoprime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`primitiveRootsPowEquiv_apply_coe` 📖	mathematical	`Nat.ModEq`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `primitiveRoots` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `primitiveRootsPowEquiv` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`primitiveRootsPowEquiv_symm_apply_coe` 📖	mathematical	`Nat.ModEq`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `primitiveRoots` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `primitiveRootsPowEquiv` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`primitiveRoots_one` 📖	mathematical	—	`primitiveRoots` `Finset` `Finset.instSingleton` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Finset.eq_singleton_iff_unique_mem` `mem_primitiveRoots` `zero_lt_one` `Nat.instZeroLEOneClass` `one_right_iff`
`sub_one_ne_zero` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid`	—	—	`sub_ne_zero` `ne_one`
`unique` 📖	—	`IsPrimitiveRoot`	—	—	`dvd_of_pow_eq_one` `pow_eq_one`
`val_inv_toRootsOfUnity_coe` 📖	mathematical	`IsPrimitiveRoot`	`Units.val` `CommMonoid.toMonoid` `Units` `Units.instInv` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `toRootsOfUnity` `Monoid.toNatPow`	—	`inv_one` `mul_one`
`val_toRootsOfUnity_coe` 📖	mathematical	`IsPrimitiveRoot`	`Units.val` `CommMonoid.toMonoid` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `toRootsOfUnity`	—	—
`zero` 📖	mathematical	—	`IsPrimitiveRoot` `CommMonoidWithZero.toCommMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`pow_zero` `zero_pow_eq` `NeZero.one`
`zmodEquivZPowers_apply_coe_int` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `ZMod` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `Additive.add` `Subgroup.mul` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `zmodEquivZPowers` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Equiv` `Equiv.instEquivLike` `Additive.ofMul` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`ZMod.intCast_rightInverse` `zmodEquivZPowers.eq_1` `AddEquiv.ofBijective_apply` `AddMonoidHom.liftOfRightInverse_comp_apply`
`zmodEquivZPowers_apply_coe_nat` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `ZMod` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `Additive.add` `Subgroup.mul` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `zmodEquivZPowers` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Equiv` `Equiv.instEquivLike` `Additive.ofMul` `Monoid.toNatPow` `Units.instMonoid`	—	`Int.cast_natCast` `zpow_natCast` `zmodEquivZPowers_apply_coe_int`
`zmodEquivZPowers_symm_apply_pow` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `ZMod` `Additive.add` `Subgroup.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmodEquivZPowers` `Equiv` `Equiv.instEquivLike` `Additive.ofMul` `Monoid.toNatPow` `Units.instMonoid` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`AddEquiv.symm_apply_apply` `zmodEquivZPowers_apply_coe_nat`
`zmodEquivZPowers_symm_apply_pow'` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `ZMod` `Additive.add` `Subgroup.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmodEquivZPowers` `Monoid.toNatPow` `Units.instMonoid` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`zmodEquivZPowers_symm_apply_pow`
`zmodEquivZPowers_symm_apply_zpow` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `ZMod` `Additive.add` `Subgroup.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmodEquivZPowers` `Equiv` `Equiv.instEquivLike` `Additive.ofMul` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`AddEquiv.symm_apply_apply` `zmodEquivZPowers_apply_coe_int`
`zmodEquivZPowers_symm_apply_zpow'` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`DFunLike.coe` `AddEquiv` `Additive` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `ZMod` `Additive.add` `Subgroup.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmodEquivZPowers` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`zmodEquivZPowers_symm_apply_zpow`
`zpow_eq_one` 📖	mathematical	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid`	`DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`zpow_natCast` `pow_eq_one`
`zpow_eq_one_iff_dvd` 📖	mathematical	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid`	`DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `pow_eq_one_iff_dvd` `LT.lt.le` `dvd_neg` `zpow_neg` `inv_one`
`zpow_of_gcd_eq_one` 📖	mathematical	`IsPrimitiveRoot` `DivisionCommMonoid.toCommMonoid`	`DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `pow_of_coprime` `LT.lt.le` `inv_iff` `zpow_neg`
`zpowers_eq` 📖	mathematical	`IsPrimitiveRoot` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid`	`Subgroup.zpowers` `Units.instGroup` `rootsOfUnity`	—	`SetLike.coe_injective` `Set.eq_of_subset_of_card_le` `Subgroup.zpowers_le_of_mem` `pow_eq_one` `card_rootsOfUnity` `ZMod.card` `Fintype.card_congr`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_monoidHom_apply_ne_one` 📖	—	`IsPrimitiveRoot`	—	—	`Nat.card_eq_fintype_card` `Fintype.card_multiplicative` `card` `IsCyclic.exists_apply_ne_one` `isCyclic_multiplicative` `instIsAddCyclic` `instFiniteMultiplicative` `Finite.of_fintype` `IsPrimitiveRoot.coe_units_iff`

(root)

Definitions

Name	Category	Theorems
`IsPrimitiveRoot` 📖	CompData	39 math math: `IsPrimitiveRoot.orderOf`, `IsPrimitiveRoot.inv_iff`, `Complex.isPrimitiveRoot_exp_rat`, `HasEnoughRootsOfUnity.prim`, `IsPrimitiveRoot.iff_def`, `isPrimitiveRoot_of_mem_rootsOfUnity`, `IsPrimitiveRoot.one`, `IsPrimitiveRoot.exists_pos`, `IsPrimitiveRoot.mk_of_lt`, `IsPrimitiveRoot.not_iff`, `Complex.isPrimitiveRoot_iff`, `IsCyclotomicExtension.exists_isPrimitiveRoot`, `Complex.isPrimitiveRoot_exp_of_isCoprime`, `Polynomial.isRoot_cyclotomic_iff_charZero`, `IsPrimitiveRoot.coe_units_iff`, `IsPrimitiveRoot.map_iff_of_injective`, `HasEnoughRootsOfUnity.exists_primitiveRoot`, `Complex.isPrimitiveRoot_exp_of_coprime`, `IsCyclotomicExtension.iff_singleton`, `Complex.isPrimitiveRoot_exp_rat_of_even_num`, `Complex.isPrimitiveRoot_exp`, `IsPrimitiveRoot.iff_orderOf`, `IsPrimitiveRoot.one_right_iff`, `IsPrimitiveRoot.coe_submonoidClass_iff`, `isCyclotomicExtension_iff`, `Complex.isPrimitiveRoot_exp_rat_of_odd_num`, `IsPrimitiveRoot.iff`, `mem_primitiveRoots`, `IsCyclotomicExtension.zeta_spec`, `IsPrimitiveRoot.zero`, `IsCyclotomicExtension.iff_adjoin_eq_top`, `IsPrimitiveRoot.neg_one`, `card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot`, `isPrimitiveRoot_of_mem_primitiveRoots`, `IsPrimitiveRoot.of_subsingleton`, `IsPrimitiveRoot.existsUnique`, `Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP`, `Polynomial.isPrimitiveRoot_of_mahlerMeasure_eq_one`, `Polynomial.isRoot_cyclotomic_iff`
`primitiveRoots` 📖	CompOp	16 math math: `IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots`, `IsPrimitiveRoot.is_roots_of_minpoly`, `Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots`, `Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots`, `IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe`, `primitiveRoots_zero`, `IsPrimitiveRoot.disjoint`, `IsPrimitiveRoot.card_primitiveRoots`, `Polynomial.cyclotomic.roots_eq_primitiveRoots_val`, `IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime_apply_coe`, `IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe`, `Complex.card_primitiveRoots`, `IsPrimitiveRoot.primitiveRoots_one`, `mem_primitiveRoots`, `IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe`, `Polynomial.roots_of_cyclotomic`
`rootsOfUnityEquivOfPrimitiveRoots` 📖	CompOp	3 math math: `rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val`, `val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe`, `rootsOfUnityEquivOfPrimitiveRoots_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot` 📖	mathematical	—	`Fintype.card` `Units` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `rootsOfUnity.fintype` `IsPrimitiveRoot`	—	`IsCyclic.exists_ofOrder_eq_natCard` `rootsOfUnity.isCyclic` `IsPrimitiveRoot.coe_units_iff` `IsPrimitiveRoot.coe_submonoidClass_iff` `IsPrimitiveRoot.iff_orderOf` `Nat.card_eq_fintype_card` `IsPrimitiveRoot.card_rootsOfUnity`
`isPrimitiveRoot_of_mem_primitiveRoots` 📖	mathematical	`Finset` `Finset.instMembership` `primitiveRoots`	`IsPrimitiveRoot` `CommRing.toCommMonoid`	—	`primitiveRoots.congr_simp` `primitiveRoots_zero` `mem_primitiveRoots`
`isPrimitiveRoot_of_mem_rootsOfUnity` 📖	mathematical	`Units` `CommMonoid.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity`	`IsPrimitiveRoot` `CommGroup.toCommMonoid` `Units.instCommGroupUnits`	—	`LT.lt.ne'` `IsOfFinOrder.orderOf_pos` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `isPeriodicPt_mul_iff_pow_eq_one` `orderOf_dvd_of_pow_eq_one` `IsPrimitiveRoot.orderOf`
`mem_primitiveRoots` 📖	mathematical	—	`Finset` `Finset.instMembership` `primitiveRoots` `IsPrimitiveRoot` `CommRing.toCommMonoid`	—	`primitiveRoots.eq_1` `Finset.mem_filter` `Multiset.mem_toFinset` `Polynomial.mem_nthRoots` `IsPrimitiveRoot.pow_eq_one`
`primitiveRoots_zero` 📖	mathematical	—	`primitiveRoots` `Finset` `Finset.instEmptyCollection`	—	`primitiveRoots.eq_1` `Polynomial.nthRoots_zero` `Multiset.toFinset_zero` `Finset.filter_empty`
`rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val` 📖	mathematical	`DFunLike.coe` `Finset.Nonempty` `primitiveRoots`	`Units.inv_val` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `MulEquiv` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `rootsOfUnityEquivOfPrimitiveRoots` `MonoidHomClass.toMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Set` `Set.instMembership` `SetLike.coe`	—	`Units.inv_val`
`rootsOfUnityEquivOfPrimitiveRoots_symm_apply` 📖	mathematical	`DFunLike.coe` `Finset.Nonempty` `primitiveRoots`	`Units.val` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `MulEquiv` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `rootsOfUnityEquivOfPrimitiveRoots`	—	`MulEquiv.surjective` `MulEquiv.symm_apply_apply` `val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe`
`val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe` 📖	mathematical	`DFunLike.coe` `Finset.Nonempty` `primitiveRoots`	`Units.val` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Units` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `MulEquiv` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `rootsOfUnityEquivOfPrimitiveRoots` `Set` `Set.instMembership` `SetLike.coe`	—	—

---

← Back to Index