Theorems · Theorem · number theory

IsPrimitiveRoot.associated_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 ζ - 1 is associated to any of its conjugate.

Defined in

Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingAlgebraNeZero