RamificationTheory.HilbertRamification.Higher.adjoin_le_adjoin_of_forall_fixed_imp_fixed
A pointwise stabilizer inclusion gives the reverse inclusion between the corresponding simple intermediate fields.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IntermediateField
universe u v
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {M : Type v}
variable [Field K] [Field M] [Algebra K M]Lean source · statement
theorem adjoin_le_adjoin_of_forall_fixed_imp_fixed
[FiniteDimensional K M] [IsGalois K M]
(a b : M)
(hfixed :
∀ σ : Gal(M / K), σ b = b → σ a = a) :
K⟮a⟯ ≤ K⟮b⟯