diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index 328dc76f2f9e4..11d2d5c352270 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -276,6 +276,10 @@ begin
   rw polynomial.eval_map,
 end
 
+lemma mem_root_set [field k] [algebra R k] {x : k} (hp : p ≠ 0) :
+  x ∈ p.root_set k ↔ aeval x p = 0 :=
+iff.trans multiset.mem_to_finset (mem_roots_map hp)
+
 lemma exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, is_root p x :=
 ⟨-(p.coeff 0 / p.coeff 1),
   have p.coeff 1 ≠ 0,
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index 10676ed147e90..ace93a8277fdb 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -488,6 +488,21 @@ begin
   rw [eval_sub, sub_eq_zero, ext],
 end
 
+/-- The set of distinct roots of `p` in `E`.
+
+If you have a non-separable polynomial, use `polynomial.roots` for the multiset
+where multiple roots have the appropriate multiplicity. -/
+def root_set (p : polynomial R) (S) [integral_domain S] [algebra R S] : set S :=
+(p.map (algebra_map R S)).roots.to_finset
+
+lemma root_set_def (p : polynomial R) (S) [integral_domain S] [algebra R S] :
+  p.root_set S = (p.map (algebra_map R S)).roots.to_finset :=
+rfl
+
+@[simp] lemma root_set_zero (S) [integral_domain S] [algebra R S] :
+  (0 : polynomial R).root_set S = ∅ :=
+by rw [root_set_def, polynomial.map_zero, roots_zero, to_finset_zero, finset.coe_empty]
+
 end roots
 
 theorem is_unit_iff {f : polynomial R} : is_unit f ↔ ∃ r : R, is_unit r ∧ C r = f :=
diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean
index 98248b9ff5101..9bd9232f6f8b1 100644
--- a/src/field_theory/normal.lean
+++ b/src/field_theory/normal.lean
@@ -97,7 +97,7 @@ end
 lemma alg_equiv.transfer_normal (f : E ≃ₐ[F] E') : normal F E ↔ normal F E' :=
 ⟨λ h, by exactI normal.of_alg_equiv f, λ h, by exactI normal.of_alg_equiv f.symm⟩
 
-lemma normal.of_is_splitting_field {p : polynomial F} [hFEp : is_splitting_field F E p] :
+lemma normal.of_is_splitting_field (p : polynomial F) [hFEp : is_splitting_field F E p] :
   normal F E :=
 begin
   by_cases hp : p = 0,
@@ -160,6 +160,8 @@ begin
   rw [set.image_singleton, ring_hom.algebra_map_to_algebra, adjoin_root.lift_root]
 end
 
+instance (p : polynomial F) : normal F p.splitting_field := normal.of_is_splitting_field p
+
 end normal_tower
 
 variables {F} {K} (ϕ ψ : K →ₐ[F] K) (χ ω : K ≃ₐ[F] K)
diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean
new file mode 100644
index 0000000000000..7eadcd27d4edb
--- /dev/null
+++ b/src/field_theory/polynomial_galois_group.lean
@@ -0,0 +1,237 @@
+/-
+Copyright (c) 2020 Thomas Browning and Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning and Patrick Lutz
+-/
+
+import field_theory.galois
+
+/-!
+# Galois Groups of Polynomials
+
+In this file we introduce the Galois group of a polynomial, defined as
+the automorphism group of the splitting field.
+
+## Main definitions
+
+- `gal p`: the Galois group of a polynomial p.
+- `restrict p E`: the restriction homomorphism `(E ≃ₐ[F] E) → gal p`.
+- `gal_action p E`: the action of `gal p` on the roots of `p` in `E`.
+
+## Main results
+
+- `restrict_smul`: `restrict p E` is compatible with `gal_action p E`.
+- `gal_action_hom_injective`: the action of `gal p` on the roots of `p` in `E` is faithful.
+- `restrict_prod_inj`: `gal (p * q)` embeds as a subgroup of `gal p × gal q`.
+-/
+
+noncomputable theory
+open_locale classical
+
+open finite_dimensional
+
+namespace polynomial
+
+variables {F : Type*} [field F] (p q : polynomial F) (E : Type*) [field E] [algebra F E]
+
+/-- The Galois group of a polynomial -/
+@[derive [has_coe_to_fun, group, fintype]]
+def gal := p.splitting_field ≃ₐ[F] p.splitting_field
+
+namespace gal
+
+instance [h : fact (p.splits (ring_hom.id F))] : unique p.gal :=
+{ default := 1,
+  uniq := λ f, alg_equiv.ext (λ x, by { obtain ⟨y, rfl⟩ := algebra.mem_bot.mp
+    ((subalgebra.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h) x).mp algebra.mem_top),
+    rw [alg_equiv.commutes, alg_equiv.commutes] }) }
+
+instance : unique (0 : polynomial F).gal :=
+begin
+  haveI : fact ((0 : polynomial F).splits (ring_hom.id F)) := splits_zero _,
+  apply_instance,
+end
+
+instance [h : fact (p.splits (algebra_map F E))] : algebra p.splitting_field E :=
+(is_splitting_field.lift p.splitting_field p h).to_ring_hom.to_algebra
+
+instance [h : fact (p.splits (algebra_map F E))] : is_scalar_tower F p.splitting_field E :=
+is_scalar_tower.of_algebra_map_eq
+  (λ x, ((is_splitting_field.lift p.splitting_field p h).commutes x).symm)
+
+/-- The restriction homomorphism -/
+def restrict [h : fact (p.splits (algebra_map F E))] : (E ≃ₐ[F] E) →* p.gal :=
+alg_equiv.restrict_normal_hom p.splitting_field
+
+section roots_action
+
+/-- The function from `roots p p.splitting_field` to `roots p E` -/
+def map_roots [h : fact (p.splits (algebra_map F E))] :
+  root_set p p.splitting_field → root_set p E :=
+λ x, ⟨is_scalar_tower.to_alg_hom F p.splitting_field E x, begin
+  have key := subtype.mem x,
+  by_cases p = 0,
+  { simp only [h, root_set_zero] at key,
+    exact false.rec _ key },
+  { rw [mem_root_set h, aeval_alg_hom_apply, (mem_root_set h).mp key, alg_hom.map_zero] } end⟩
+
+lemma map_roots_bijective [h : fact (p.splits (algebra_map F E))] :
+  function.bijective (map_roots p E) :=
+begin
+  split,
+  { exact λ _ _ h, subtype.ext (ring_hom.injective _ (subtype.ext_iff.mp h)) },
+  { intro y,
+    have key := roots_map
+      (is_scalar_tower.to_alg_hom F p.splitting_field E : p.splitting_field →+* E)
+      ((splits_id_iff_splits _).mpr (is_splitting_field.splits p.splitting_field p)),
+    rw [map_map, alg_hom.comp_algebra_map] at key,
+    have hy := subtype.mem y,
+    simp only [root_set, finset.mem_coe, multiset.mem_to_finset, key, multiset.mem_map] at hy,
+    rcases hy with ⟨x, hx1, hx2⟩,
+    exact ⟨⟨x, multiset.mem_to_finset.mpr hx1⟩, subtype.ext hx2⟩ }
+end
+
+/-- The bijection between `root_set p p.splitting_field` and `root_set p E` -/
+def roots_equiv_roots [h : fact (p.splits (algebra_map F E))] :
+  (root_set p p.splitting_field) ≃ (root_set p E) :=
+equiv.of_bijective (map_roots p E) (map_roots_bijective p E)
+
+instance gal_action_aux : mul_action p.gal (root_set p p.splitting_field) :=
+{ smul := λ ϕ x, ⟨ϕ x, begin
+    have key := subtype.mem x,
+    --simp only [root_set, finset.mem_coe, multiset.mem_to_finset] at *,
+    by_cases p = 0,
+    { simp only [h, root_set_zero] at key,
+      exact false.rec _ key },
+    { rw mem_root_set h,
+      change aeval (ϕ.to_alg_hom x) p = 0,
+      rw [aeval_alg_hom_apply, (mem_root_set h).mp key, alg_hom.map_zero] } end⟩,
+  one_smul := λ _, by { ext, refl },
+  mul_smul := λ _ _ _, by { ext, refl } }
+
+instance gal_action [h : fact (p.splits (algebra_map F E))] : mul_action p.gal (root_set p E) :=
+{ smul := λ ϕ x, roots_equiv_roots p E (ϕ • ((roots_equiv_roots p E).symm x)),
+  one_smul := λ _, by simp only [equiv.apply_symm_apply, one_smul],
+  mul_smul := λ _ _ _, by simp only [equiv.apply_symm_apply, equiv.symm_apply_apply, mul_smul] }
+
+variables {p E}
+
+@[simp] lemma restrict_smul [h : fact (p.splits (algebra_map F E))]
+  (ϕ : E ≃ₐ[F] E) (x : root_set p E) : ↑((restrict p E ϕ) • x) = ϕ x :=
+begin
+  let ψ := alg_hom.alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F p.splitting_field E),
+  change ↑(ψ (ψ.symm _)) = ϕ x,
+  rw alg_equiv.apply_symm_apply ψ,
+  change ϕ (roots_equiv_roots p E ((roots_equiv_roots p E).symm x)) = ϕ x,
+  rw equiv.apply_symm_apply (roots_equiv_roots p E),
+end
+
+variables (p E)
+
+/-- `gal_action` as a permutation representation -/
+def gal_action_hom [h : fact (p.splits (algebra_map F E))] : p.gal →* equiv.perm (root_set p E) :=
+{ to_fun := λ ϕ, equiv.mk (λ x, ϕ • x) (λ x, ϕ⁻¹ • x)
+  (λ x, inv_smul_smul ϕ x) (λ x, smul_inv_smul ϕ x),
+  map_one' := by { ext1 x, exact mul_action.one_smul x },
+  map_mul' := λ x y, by { ext1 z, exact mul_action.mul_smul x y z } }
+
+lemma gal_action_hom_injective [h : fact (p.splits (algebra_map F E))] :
+  function.injective (gal_action_hom p E) :=
+begin
+  rw monoid_hom.injective_iff,
+  intros ϕ hϕ,
+  let equalizer := alg_hom.equalizer ϕ.to_alg_hom (alg_hom.id F p.splitting_field),
+  suffices : equalizer = ⊤,
+  { exact alg_equiv.ext (λ x, (subalgebra.ext_iff.mp this x).mpr algebra.mem_top) },
+  rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff],
+  intros x hx,
+  have key := equiv.perm.ext_iff.mp hϕ (roots_equiv_roots p E ⟨x, hx⟩),
+  change roots_equiv_roots p E (ϕ • (roots_equiv_roots p E).symm
+    (roots_equiv_roots p E ⟨x, hx⟩)) = roots_equiv_roots p E ⟨x, hx⟩ at key,
+  rw equiv.symm_apply_apply at key,
+  exact subtype.ext_iff.mp (equiv.injective (roots_equiv_roots p E) key),
+end
+
+end roots_action
+
+variables {p q}
+
+/-- The restriction homomorphism between Galois groups -/
+def restrict_dvd (hpq : p ∣ q) : q.gal →* p.gal :=
+if hq : q = 0 then 1 else @restrict F _ p _ _ _
+  (splits_of_splits_of_dvd (algebra_map F q.splitting_field) hq (splitting_field.splits q) hpq)
+
+variables (p q)
+
+/-- The Galois group of a product embeds into the product of the Galois groups  -/
+def restrict_prod : (p * q).gal →* p.gal × q.gal :=
+monoid_hom.prod (restrict_dvd (dvd_mul_right p q)) (restrict_dvd (dvd_mul_left q p))
+
+lemma restrict_prod_injective : function.injective (restrict_prod p q) :=
+begin
+  by_cases hpq : (p * q) = 0,
+  { haveI : unique (gal (p * q)) := by { rw hpq, apply_instance },
+    exact λ f g h, eq.trans (unique.eq_default f) (unique.eq_default g).symm },
+  intros f g hfg,
+  dsimp only [restrict_prod, restrict_dvd] at hfg,
+  simp only [dif_neg hpq, monoid_hom.prod_apply, prod.mk.inj_iff] at hfg,
+  suffices : alg_hom.equalizer f.to_alg_hom g.to_alg_hom = ⊤,
+  { exact alg_equiv.ext (λ x, (subalgebra.ext_iff.mp this x).mpr algebra.mem_top) },
+  rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff],
+  intros x hx,
+  rw [map_mul, polynomial.roots_mul] at hx,
+  cases multiset.mem_add.mp (multiset.mem_to_finset.mp hx) with h h,
+  { change f x = g x,
+    haveI : fact (p.splits (algebra_map F (p * q).splitting_field)) :=
+      splits_of_splits_of_dvd _ hpq (splitting_field.splits (p * q)) (dvd_mul_right p q),
+    have key : x = algebra_map (p.splitting_field) (p * q).splitting_field
+      ((roots_equiv_roots p _).inv_fun ⟨x, multiset.mem_to_finset.mpr h⟩) :=
+      subtype.ext_iff.mp (equiv.apply_symm_apply (roots_equiv_roots p _) ⟨x, _⟩).symm,
+    rw [key, ←alg_equiv.restrict_normal_commutes, ←alg_equiv.restrict_normal_commutes],
+    exact congr_arg _ (alg_equiv.ext_iff.mp hfg.1 _) },
+  { change f x = g x,
+    haveI : fact (q.splits (algebra_map F (p * q).splitting_field)) :=
+      splits_of_splits_of_dvd _ hpq (splitting_field.splits (p * q)) (dvd_mul_left q p),
+    have key : x = algebra_map (q.splitting_field) (p * q).splitting_field
+      ((roots_equiv_roots q _).inv_fun ⟨x, multiset.mem_to_finset.mpr h⟩) :=
+      subtype.ext_iff.mp (equiv.apply_symm_apply (roots_equiv_roots q _) ⟨x, _⟩).symm,
+    rw [key, ←alg_equiv.restrict_normal_commutes, ←alg_equiv.restrict_normal_commutes],
+    exact congr_arg _ (alg_equiv.ext_iff.mp hfg.2 _) },
+  { rwa [ne.def, mul_eq_zero, map_eq_zero, map_eq_zero, ←mul_eq_zero] }
+end
+
+variables {p q}
+
+lemma card_of_separable (hp : p.separable) :
+  fintype.card p.gal = findim F p.splitting_field :=
+begin
+  haveI : is_galois F p.splitting_field := is_galois.of_separable_splitting_field hp,
+  exact is_galois.card_aut_eq_findim F p.splitting_field,
+end
+
+lemma prime_degree_dvd_card [char_zero F] (p_irr : irreducible p) (p_deg : p.nat_degree.prime) :
+  p.nat_degree ∣ fintype.card p.gal :=
+begin
+  rw gal.card_of_separable p_irr.separable,
+  have hp : p.degree ≠ 0 :=
+    λ h, nat.prime.ne_zero p_deg (nat_degree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h)),
+  let α : p.splitting_field := root_of_splits (algebra_map F p.splitting_field)
+    (splitting_field.splits p) hp,
+  have hα : is_integral F α :=
+    (is_algebraic_iff_is_integral F).mp (algebra.is_algebraic_of_finite α),
+  use finite_dimensional.findim F⟮α⟯ p.splitting_field,
+  suffices : (minpoly F α).nat_degree = p.nat_degree,
+  { rw [←finite_dimensional.findim_mul_findim F F⟮α⟯ p.splitting_field,
+        intermediate_field.adjoin.findim hα, this] },
+  suffices : minpoly F α ∣ p,
+  { have key := dvd_symm_of_irreducible (minpoly.irreducible hα) p_irr this,
+    apply le_antisymm,
+    { exact nat_degree_le_of_dvd this p_irr.ne_zero },
+    { exact nat_degree_le_of_dvd key (minpoly.ne_zero hα) } },
+  apply minpoly.dvd F α,
+  rw [aeval_def, map_root_of_splits _ (splitting_field.splits p) hp],
+end
+
+end gal
+
+end polynomial
diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean
index facc9f4764d64..de93dcf5ce3ab 100644
--- a/src/field_theory/splitting_field.lean
+++ b/src/field_theory/splitting_field.lean
@@ -641,6 +641,9 @@ theorem adjoin_roots : algebra.adjoin α
     (↑(f.map (algebra_map α $ splitting_field f)).roots.to_finset : set (splitting_field f)) = ⊤ :=
 splitting_field_aux.adjoin_roots _ _ _
 
+theorem adjoin_root_set : algebra.adjoin α (f.root_set f.splitting_field) = ⊤ :=
+adjoin_roots f
+
 end splitting_field
 
 variables (α β) [algebra α β]
@@ -716,6 +719,9 @@ finite_dimensional.iff_fg.2 $ @algebra.coe_top α β _ _ _ ▸ adjoin_roots β f
   else (is_algebraic_iff_is_integral _).1 ⟨f, hf, (eval₂_eq_eval_map _).trans $
     (mem_roots $ by exact map_ne_zero hf).1 (multiset.mem_to_finset.mp hy)⟩)
 
+instance (f : polynomial α) : _root_.finite_dimensional α f.splitting_field :=
+finite_dimensional f.splitting_field f
+
 /-- Any splitting field is isomorphic to `splitting_field f`. -/
 def alg_equiv (f : polynomial α) [is_splitting_field α β f] : β ≃ₐ[α] splitting_field f :=
 begin