ArtinSchreierTheory.exists_nontrivial_character_of_artinSchreier_not_surjective
A failed Artin–Schreier equation gives a nontrivial continuous prime cyclic character.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ArtinSchreierTheory
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω]
[CharP Ω p] [Algebra K Ω] [IsGalois K Ω] [IsSepClosed Ω]Lean source · statement
theorem exists_nontrivial_character_of_artinSchreier_not_surjective
(hAS : ∃ a : K, ∀ x : K, x ^ p - x ≠ a) :
∃ χ : Gal(Ω/K) →ₜ* Multiplicative (ZMod p), ∃ σ : Gal(Ω/K), χ σ ≠ 1