Theorems · Theorem · number theory

NumberField.Units.rootsOfUnity_eq_one

∀ (K : Type u_1) [inst : Field K] {k : ℕ+},
  (↑k).Coprime (NumberField.Units.torsionOrder K) →
    ∀ {ζ : (NumberField.RingOfIntegers K)ˣ}, ζ ∈ rootsOfUnity (↑k) (NumberField.RingOfIntegers K) ↔ ζ = 1

If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.

Defined in

Mathlib.NumberTheory.NumberField.Units.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field