Module

CyclotomicGaloisCard.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicGaloisCard

2 declarations indexed from sourceView source ↗

Module documentation

Prime-order cyclotomic extensions have prime-to-prime Galois groups

The action on a primitive root embeds the automorphism group into the units of ZMod p. The primitive root and its generating property come from the cyclotomic extension itself; no irreducibility assumption is needed.

Imports4

Mathlib.NumberTheory.Cyclotomic.Gal
Mathlib.GroupTheory.Coset.Card
Mathlib.Data.Nat.Totient
Mathlib.Data.Nat.GCD.Basic

Imported by8

theorem

cyclotomicGalois_natCard_dvd_prime_sub_one

L27 ↗

ValuationTheory.DiscreteValuationField.cyclotomicGalois_natCard_dvd_prime_sub_one

Documentation

The Galois group of an extension generated by the p-th roots of unity has order dividing p - 1.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.DiscreteValuationField
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
    (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K L]

Lean source · statement

theorem cyclotomicGalois_natCard_dvd_prime_sub_one :
    Nat.card (L ≃ₐ[K] L) ∣ p - 1

theorem

prime_coprime_cyclotomicGalois_natCard

L39 ↗

ValuationTheory.DiscreteValuationField.prime_coprime_cyclotomicGalois_natCard