RamificationTheory.HilbertRamification.ValuationSubring.exists_primitiveRoot_residue_of_inertia_prime_order
In residue characteristic zero, a nontrivial inertia element of prime order forces a primitive root of that order in the actual residue field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]Lean source · statement
theorem exists_primitiveRoot_residue_of_inertia_prime_order
(A : _root_.ValuationSubring L) [Finite (inertiaGroup K A)]
[CharZero (IsLocalRing.ResidueField A)]
{p : ℕ} (hp : p.Prime) (σ : inertiaGroup K A)
(hσ : σ ≠ 1) (hpow : σ ^ p = 1) :
(primitiveRoots p (IsLocalRing.ResidueField A)).Nonempty