From 4ded5ca36a4f73bc4d04ed91dc96d391a239bd16 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 10 Apr 2022 23:04:52 +0000 Subject: [PATCH] fix(field_theory/galois): update docstring (#13188) --- src/field_theory/galois.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean index a89dda44b9d48..22f5c16445623 100644 --- a/src/field_theory/galois.lean +++ b/src/field_theory/galois.lean @@ -24,11 +24,12 @@ In this file we define Galois extensions as extensions which are both separable ## Main results -- `fixing_subgroup_of_fixed_field` : If `E/F` is finite dimensional (but not necessarily Galois) - then `fixing_subgroup (fixed_field H) = H` -- `fixed_field_of_fixing_subgroup`: If `E/F` is finite dimensional and Galois +- `intermediate_field.fixing_subgroup_fixed_field` : If `E/F` is finite dimensional (but not + necessarily Galois) then `fixing_subgroup (fixed_field H) = H` +- `intermediate_field.fixed_field_fixing_subgroup`: If `E/F` is finite dimensional and Galois then `fixed_field (fixing_subgroup K) = K` -Together, these two result prove the Galois correspondence + +Together, these two results prove the Galois correspondence. - `is_galois.tfae` : Equivalent characterizations of a Galois extension of finite degree -/