Skip to content

Commit

Permalink
fix(field_theory/galois): update docstring (#13188)
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Apr 10, 2022
1 parent be22d07 commit 4ded5ca
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions src/field_theory/galois.lean
Expand Up @@ -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
-/
Expand Down

0 comments on commit 4ded5ca

Please sign in to comment.