feat(field_theory/abel_ruffini): Version of solvable_by_rad.is_solvab…

…le (#7509)

This is a version of `solvable_by_rad.is_solvable`, which will be the final step of the abel-ruffini theorem.

src/field_theory/abel_ruffini.lean

@@ -372,6 +372,21 @@ begin
   { exact λ α n, induction3 },
 end
 
+/-- An irreducible polynomial with an `is_solvable_by_rad` root has solvable Galois group -/
+lemma is_solvable' {α : E} {q : polynomial F} (q_irred : irreducible q)
+  (q_aeval : aeval α q = 0) (hα : is_solvable_by_rad F α) :
+  _root_.is_solvable q.gal :=
+begin
+  haveI : _root_.is_solvable (q * C q.leading_coeff⁻¹).gal := by
+  { rw [minpoly.unique'' q_irred q_aeval,
+        ←show minpoly F (⟨α, hα⟩ : solvable_by_rad F E) = minpoly F α,
+        from minpoly.eq_of_algebra_map_eq (ring_hom.injective _) (is_integral ⟨α, hα⟩) rfl],
+    exact is_solvable ⟨α, hα⟩ },
+  refine solvable_of_surjective (gal.restrict_dvd_surjective ⟨C q.leading_coeff⁻¹, rfl⟩ _),
+  rw [mul_ne_zero_iff, ne, ne, C_eq_zero, inv_eq_zero],
+  exact ⟨q_irred.ne_zero, leading_coeff_ne_zero.mpr q_irred.ne_zero⟩,
+end
+
 end solvable_by_rad
 
 end abel_ruffini

src/field_theory/minpoly.lean

@@ -293,6 +293,18 @@ eq_of_monic_of_associated hp3 (monic ⟨p, ⟨hp3, hp2⟩⟩) $
 mul_one (minpoly A x) ▸ hq.symm ▸ associated_mul_mul (associated.refl _) $
 associated_one_iff_is_unit.2 $ (hp1.is_unit_or_is_unit hq).resolve_left $ not_is_unit A x
 
+lemma unique'' [nontrivial B] {p : polynomial A}
+  (hp1 : _root_.irreducible p) (hp2 : polynomial.aeval x p = 0) :
+  p * C p.leading_coeff⁻¹ = minpoly A x :=
+begin
+  have : p.leading_coeff ≠ 0 := leading_coeff_ne_zero.mpr hp1.ne_zero,
+  apply unique',
+  { exact irreducible_of_associated ⟨⟨C p.leading_coeff⁻¹, C p.leading_coeff,
+      by rwa [←C_mul, inv_mul_cancel, C_1], by rwa [←C_mul, mul_inv_cancel, C_1]⟩, rfl⟩ hp1 },
+  { rw [aeval_mul, hp2, zero_mul] },
+  { rwa [polynomial.monic, leading_coeff_mul, leading_coeff_C, mul_inv_cancel] },
+end
+
 /-- If `y` is the image of `x` in an extension, their minimal polynomials coincide.
 
 We take `h : y = algebra_map L T x` as an argument because `rw h` typically fails