Theorems · Theorem · number theory

IsPrimitiveRoot.lcm_totient_le_finrank

∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra K L]
  [FiniteDimensional K L] {p q : ℕ} {x y : L},
  IsPrimitiveRoot x p →
    IsPrimitiveRoot y q → Irreducible (Polynomial.cyclotomic (p.lcm q) K) → (p.lcm q).totient ≤ Module.finrank K L

If L contains both a primitive p-th root of unity and q-th root of unity, and Irreducible (cyclotomic (lcm p q) K) (in particular for K = ℚ), then the finrank K L is at least (lcm p q).totient.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCommRingIsDomainAlgebraFiniteDimensional