Theorems · Theorem · number theory

IsPrimitiveRoot.associated_map_sub_one_map_sub_one

∀ {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A] {R : Type u_3} [inst_2 : CommRing R] [inst_3 : Algebra R A]
  {n : ℕ} [NeZero n], IsPrimitiveRoot ζ n → ∀ (σ τ : A ≃ₐ[R] A), Associated (σ (ζ - 1)) (τ (ζ - 1))

Given an n-th primitive root of unity ζ, we have that two conjugates of ζ - 1 are associated.

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingAlgebraNeZero