Yamaguchi26AbfaithfulGalois.exists_infinite_formalHilbert90_orientation_of_cyclic_extension
A cyclic degree-p extension supplies the infinite orientation required in Corollary 6.6. Prime degree makes the finite Galois group cyclic automatically.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe uLean source · statement
theorem exists_infinite_formalHilbert90_orientation_of_cyclic_extension
(p : ℕ) [Fact p.Prime] (K : Type u) [Field K] [CharP K p]
(L : IntermediateField K (SeparableClosure K)) [IsGalois K L]
(hdegree : Module.finrank K L = p) :
∃ θ : Orientation p Gal(AlgebraicClosure K/K),
FormalHilbert90 θ ∧ Set.Infinite (Set.range θ)