Theorems · Definition · number theory

IsCyclotomicExtension.Rat.galEquivZMod

(n : ℕ) →
  [NeZero n] →
    (K : Type u_1) →
      [inst : Field K] → [inst_1 : NumberField K] → [hK : IsCyclotomicExtension {n} ℚ K] → Gal(K/ℚ) ≃* (ZMod n)ˣ

The isomorphism between Gal(ℚ(ζₙ)/ℚ) and (ℤ/nℤ)ˣ that sends σ to the class a such that σ (ζₙ) = ζₙ ^ a.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Cited by

11 results in Mathlib

Foundations

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

Assumes

NeZeroFieldNumberFieldIsCyclotomicExtension