Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.torsionOrder_eq

∀ {n : ℕ} {K : Type u} [inst : Field K] [NeZero n] [inst_2 : NumberField K] [hK : IsCyclotomicExtension {n} ℚ K],
  NumberField.Units.torsionOrder K = if Even n then n else 2 * n

The order of the torsion group of the n-th cyclotomic field is n if n is even and 2n if n is odd.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNeZeroNumberFieldIsCyclotomicExtension