Module

CyclotomicAutToPowReduction.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicAutToPowReduction

1 declaration indexed from sourceView source ↗

Module documentation

Reduction of the action on primitive roots

The exponent of an automorphism on a primitive p-power root reduces to its exponent on any primitive p-th root in the same field. The two roots need not be chosen compatibly.

Imports4

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Mathlib.Data.ZMod.Units
Mathlib.Data.Nat.Prime.Basic
Mathlib.GroupTheory.OrderOfElement

Imported by2

theorem

autToPow_unitsMap_prime_pow

L26 ↗

ValuationTheory.DiscreteValuationField.autToPow_unitsMap_prime_pow

Documentation

The finite cyclotomic action on a primitive p^(s+1)-th root reduces to the action on any primitive p-th root.

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]

Lean source · statement

theorem autToPow_unitsMap_prime_pow (p s : ℕ) [Fact p.Prime]
    {ζ η : L} (hζ : IsPrimitiveRoot ζ (p ^ (s + 1)))
    (hη : IsPrimitiveRoot η p) (σ : L ≃ₐ[K] L) :
    ZMod.unitsMap (dvd_pow_self p (Nat.succ_ne_zero s)) (hζ.autToPow K σ) =
      hη.autToPow K σ

Module documentation

Reduction of the action on primitive roots

Declarations

autToPow_unitsMap_prime_pow