Theorems · Theorem · number theory

IsPrimitiveRoot.adjoin_pair_eq

∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] (S : Type u_7) [inst_2 : CommSemiring S] [inst_3 : Algebra S R]
  {ζ₁ ζ₂ : R} {k₁ k₂ : ℕ},
  IsPrimitiveRoot ζ₁ k₁ →
    IsPrimitiveRoot ζ₂ k₂ → k₁ ≠ 0 → k₂ ≠ 0 → ∀ {ζ : R}, IsPrimitiveRoot ζ (k₁.lcm k₂) → S[ζ₁, ζ₂] = S[ζ]

The sub-algebra generated by two roots of unity of order k₁ and k₂ resp. is the same as the one generated by a root of unity of order lcm k₁ k₂. See IsPrimitiveRoot.pow_mul_pow_lcm for how to construct a root of unity of order lcm k₁ k₂ from roots of unity of order k₁ and k₂.

Defined in

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommSemiringAlgebra