Theorems · Theorem · number theory

IsPrimitiveRoot.geom_sum_isUnit

∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → 2 ≤ n → j.Coprime n → IsUnit (∑ i ∈ Finset.range j, ζ ^ i)

Given an n-th primitive root of unity ζ, where 2 ≤ n, we have that ∑ i ∈ range j, ζ ^ i is a unit for all j coprime with n. This is the unit given by associated_pow_sub_one_pow_of_coprime (see pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum).

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain