KummerTheory.exists_moving_primitiveRoot_of_not_all_roots_in_base
A primitive root is moved by a Galois automorphism when the roots at its level do not all come from the base field.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
variable (L E : Type*) [Field L] [Field E] [Algebra L E]
[FiniteDimensional L E] [IsGalois L E]Lean source · statement
theorem exists_moving_primitiveRoot_of_not_all_roots_in_base
(m : ℕ+) (hmu : (primitiveRoots (m : ℕ) E).Nonempty)
(hnot : ¬ ∀ ξ : E, ξ ^ (m : ℕ) = 1 →
ξ ∈ Set.range (algebraMap L E)) :
∃ (ζ : E) (τ : Gal(E/L)), IsPrimitiveRoot ζ (m : ℕ) ∧ τ ζ ≠ ζ