Theorems · Theorem · number theory

IsCyclotomicExtension.finrank

∀ {n : ℕ} [NeZero n] {K : Type u} (L : Type v) [inst : Field K] [inst_1 : CommRing L] [IsDomain L]
  [inst_3 : Algebra K L] [IsCyclotomicExtension {n} K L],
  Irreducible (Polynomial.cyclotomic n K) → Module.finrank K L = n.totient

If Irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

12 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCommRingIsDomainAlgebraIsCyclotomicExtension