Theorems · Theorem · number theory

IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime

Deprecated since 2026-06-23Use IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime instead.

∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
  IsPrimitiveRoot ζ p →
    Nat.Prime p → (↑(Polynomial.nthRootsFinset p 1)).Pairwise fun η₁ η₂ => Associated (ζ - 1) (η₁ - η₂)

Alias of IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime. If p is prime and ζ is a p-th primitive root of unity, then ζ - 1 and η₁ - η₂ are associated for all distinct p-th roots of unity η₁ and η₂.

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain