Module

RootOfUnityPowerAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.RootOfUnityPowerAction

1 declaration indexed from sourceView source ↗

Module documentation

The bounded power describing an automorphism of roots of unity

The image of a primitive root is primitive. Its bounded exponent is therefore coprime to the order and describes the action on every root at that order.

Imports2

Mathlib.Data.PNat.Defs
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by3

theorem

exists_bounded_coprime_power_action_on_roots

L21 ↗

KummerTheory.exists_bounded_coprime_power_action_on_roots

Documentation

A field automorphism acts on all roots at a primitive-root level by one bounded exponent coprime to that level.

Source context 1 command

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

namespace KummerTheory

Lean source · statement

theorem exists_bounded_coprime_power_action_on_roots
    (K : Type*) [Field K] (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (τ : K ≃+* K) :
    ∃ a : ℕ, a < (n : ℕ) ∧ a.Coprime (n : ℕ) ∧
      ∀ ζ : K, ζ ^ (n : ℕ) = 1 → τ ζ = ζ ^ a

Module documentation

The bounded power describing an automorphism of roots of unity

Declarations

exists_bounded_coprime_power_action_on_roots