ArtinSchreierTheory.exists_moved_class_of_degree_eq_char
A degree-p Galois extension cannot fix all Artin–Schreier classes when the base field has infinitely many such classes.
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} {L : Type v} [Field K] [Field L]
[CharP K p] [CharP L p] [Algebra K L] [IsGalois K L]Lean source · statement
theorem exists_moved_class_of_degree_eq_char
[Infinite (K ⧸ ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range)]
(hdegree : Module.finrank K L = p) :
∃ τ : Gal(L/K), τ ≠ 1 ∧ ∃ x : L, ∀ y : L, y ^ p - y ≠ τ x - x