feat: port FieldTheory.Galois (#5115)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · Jun 16, 2023 · b33be3b · b33be3b
1 parent eae91c7
commit b33be3b
Show file tree

Hide file tree

Showing 2 changed files with 475 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1738,6 +1738,7 @@ import Mathlib.FieldTheory.Finite.Basic
 import Mathlib.FieldTheory.Finite.Polynomial
 import Mathlib.FieldTheory.Finiteness
 import Mathlib.FieldTheory.Fixed
+import Mathlib.FieldTheory.Galois
 import Mathlib.FieldTheory.IntermediateField
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.FieldTheory.IsAlgClosed.Classification