Theorems · Theorem · number theory

Polynomial.normalizedFactors_cyclotomic_card

∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] [inst_2 : DecidableEq K],
      (UniqueFactorizationMonoid.normalizedFactors (Polynomial.cyclotomic n K)).toFinset.card =
        n.totient / orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)

Let K be a finite field of cardinality p ^ f and let P be an irreducible factor of the n-th cyclotomic polynomial over K, where p and n are coprime. This result computes the number of distinct irreducible factors of cyclotomic n K.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFintypeFactDecidableEq