Roots of unity and primitive roots of unity
We define roots of unity in the context of an arbitrary commutative monoid,
as a subgroup of the group of units. We also define a predicate
is_primitive_root on commutative
monoids, expressing that an element is a primitive root of unity.
roots_of_unity n M, for
n : ℕ+is the subgroup of the units of a commutative monoid
Mconsisting of elements
x ^ n = 1.
is_primitive_root ζ k: an element
ζis a primitive
k-th root of unity if
ζ ^ k = 1, and if
ζ ^ l = 1then
k ∣ l.
primitive_roots k R: the finset of primitive
k-th roots of unity in an integral domain
roots_of_unity.is_cyclic: the roots of unity in an integral domain form a cyclic group.
zmod kis equivalent to the subgroup generated by a primitive
k-th root of unity.
is_primitive_root.gpowers_eq: in an integral domain, the subgroup generated by a primitive
k-th root of unity is equal to the
k-th roots of unity.
is_primitive_root.card_primitive_roots: if an integral domain has a primitive
k-th root of unity, then it has
φ kof them.
It is desirable that
roots_of_unity is a subgroup,
and it will mainly be applied to rings (e.g. the ring of integers in a number field) and fields.
We therefore implement it as a subgroup of the units of a commutative monoid.
On the other hand, for primitive roots of unity, it is desirable to have a predicate
not just on units, but directly on elements of the ring/field.
For example, we want to say that
exp (2 * pi * I / n) is a primitive
n-th root of unity
in the complex numbers, without having to turn that number into a unit first.
Equivalence between the
k-th roots of unity in
R and the
k-th roots of
This is implemented as equivalence of subtypes,
roots_of_unity is a subgroup of the group of units,
nth_roots is a multiset.
The (additive) monoid equivalence between
and the powers of a primitive root of unity