Skip to content

Commit

Permalink
fix layout
Browse files Browse the repository at this point in the history
delete a tab

Co-authored-by: Jz Pan <[email protected]>
  • Loading branch information
Thmoas-Guan and acmepjz authored Dec 4, 2024
1 parent 11a9ac5 commit bc7ca2b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/FieldTheory/Galois/Profinite.lean
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ variable (k K) in
/--`finGaloisGroupFunctor` composite with the forgetful functor from `FiniteGrp` to `ProfiniteGrp`-/
noncomputable abbrev profinGaloisGroupFunctor :
(FiniteGaloisIntermediateField k K)ᵒᵖ ⥤ ProfiniteGrp :=
(finGaloisGroupFunctor k K) ⋙ forget₂ FiniteGrp ProfiniteGrp
(finGaloisGroupFunctor k K) ⋙ forget₂ FiniteGrp ProfiniteGrp

variable (k K) in
/--Define the homomorphism from `Gal(K/k)` to `lim Gal(L/k)` where `L` is a
Expand Down

0 comments on commit bc7ca2b

Please sign in to comment.