Theorems · Theorem · number theory

IsPrimitiveRoot.associated_pow_add_sub_sub_one

∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → 2 ≤ n → ∀ (i : ℕ), j.Coprime n → Associated (ζ - 1) (ζ ^ (i + j) - ζ ^ i)

Given an n-th primitive root of unity ζ, where 2 ≤ n, we have that ζ - 1 and ζ ^ (i + j) - ζ ^ i are associated for all and j coprime with n and all i. See pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one for the explicit formula of the unit.

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain