EnoughRootsOfUnity

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

Statistics

Metric	Count
Definitions HasEnoughRootsOfUnity	1
Theorems cyc, exists_primitiveRoot, finite_rootsOfUnity, natCard_rootsOfUnity, of_card_le, of_dvd, prim, rootsOfUnity_isCyclic, monoidHom_equiv_self, hasEnoughRootsOfUnity, instHasEnoughRootsOfUnityOfNatNat	11
Total	12

HasEnoughRootsOfUnity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyc 📖	mathematical	—	IsCyclic Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.zpow	—	—
exists_primitiveRoot 📖	mathematical	—	IsPrimitiveRoot	—	prim
finite_rootsOfUnity 📖	mathematical	—	Finite Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	—	rootsOfUnity_isCyclic IsCyclic.exists_generator SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass OneMemClass.coe_eq_one Subtype.prop Finite.of_surjective Finite.of_fintype Subgroup.mem_zpowers_iff ZMod.natCast_val ZMod.coe_intCast zpow_eq_zpow_emod'
natCard_rootsOfUnity 📖	mathematical	—	Nat.card Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	—	exists_primitiveRoot IsCyclic.exponent_eq_card rootsOfUnity_isCyclic dvd_antisymm Nat.instIsCancelMulZero Unique.instSubsingleton Monoid.exponent_dvd_of_forall_pow_eq_one Subgroup.instSubgroupClass OneMemClass.coe_eq_one Subtype.prop IsPrimitiveRoot.eq_orderOf IsPrimitiveRoot.isUnit IsUnit.unit_spec orderOf_units Units.val_pow_eq_pow_val IsPrimitiveRoot.pow_eq_one Units.val_one Monoid.order_dvd_exponent
of_card_le 📖	mathematical	Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype	HasEnoughRootsOfUnity	—	card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot le_antisymm card_rootsOfUnity rootsOfUnity.isCyclic
of_dvd 📖	mathematical	—	HasEnoughRootsOfUnity	—	exists_primitiveRoot IsPrimitiveRoot.pow NeZero.pos Nat.instCanonicallyOrderedAdd mul_comm Subgroup.isCyclic_of_le rootsOfUnity_le_of_dvd rootsOfUnity_isCyclic
prim 📖	mathematical	—	IsPrimitiveRoot	—	—
rootsOfUnity_isCyclic 📖	mathematical	—	IsCyclic Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.zpow	—	cyc

IsCyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monoidHom_equiv_self 📖	mathematical	—	MulEquiv MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Units.instMulOneClass MonoidHom.mul CommGroup.toCommMonoid Units.instCommGroupUnits MulOne.toMul	—	LT.lt.ne' Nat.card_pos One.instNonempty HasEnoughRootsOfUnity.natCard_rootsOfUnity monoidHom_mulEquiv_rootsOfUnity HasEnoughRootsOfUnity.rootsOfUnity_isCyclic

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasEnoughRootsOfUnity 📖	mathematical	—	HasEnoughRootsOfUnity	—	HasEnoughRootsOfUnity.prim IsPrimitiveRoot.coe_units_iff SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass IsPrimitiveRoot.coe_submonoidClass_iff IsPrimitiveRoot.map_of_injective MulEquivClass.instMonoidHomClass instMulEquivClass injective isCyclic_of_surjective HasEnoughRootsOfUnity.rootsOfUnity_isCyclic surjective

(root)

Definitions

Name	Category	Theorems
HasEnoughRootsOfUnity 📖	CompData	12 math math: IsSepClosed.hasEnoughRootsOfUnity, MulEquiv.hasEnoughRootsOfUnity, HasEnoughRootsOfUnity.of_card_le, HasEnoughRootsOfUnity.of_dvd, instHasEnoughRootsOfUnityOfNatNat, AlgebraicClosure.hasEnoughRootsOfUnity, SeparableClosure.hasEnoughRootsOfUnity_pow, SeparableClosure.hasEnoughRootsOfUnity, instHasEnoughRootsOfUnityCircle, IsSepClosed.hasEnoughRootsOfUnity_pow, AlgebraicClosure.hasEnoughRootsOfUnity_pow, ZMod.instHasEnoughRootsOfUnityHSubNatOfNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasEnoughRootsOfUnityOfNatNat 📖	mathematical	—	HasEnoughRootsOfUnity	—	isCyclic_of_subsingleton instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat

---

← Back to Index