feat(field_theory/minpoly): remove is_integral requirement from `un…

…ique'` (#7064)

`unique'` had an extraneous requirement on `is_integral`, which could be inferred from the other arguments.

This is a small step towards #5258, but is a breaking change; `unique'` now needs one less argument, which will break all current code using `unique'`.

src/field_theory/abel_ruffini.lean

@@ -341,7 +341,7 @@ begin
     exact ⟨is_integral β, hpq.2⟩,
   end),
   have key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩) := minpoly.unique'
-    (normal.is_integral (splitting_field.normal _) _) (minpoly.irreducible (is_integral γ)) begin
+    (minpoly.irreducible (is_integral γ)) begin
       suffices : aeval (⟨γ, hγ⟩ : F ⟮α, β⟯) (minpoly F γ) = 0,
       { rw [aeval_alg_hom_apply, this, alg_hom.map_zero] },
       apply (algebra_map F⟮α, β⟯ (solvable_by_rad F E)).injective,

src/field_theory/fixed.lean

@@ -179,7 +179,7 @@ theorem is_integral : is_integral (fixed_points G F) x :=
 
 theorem minpoly_eq_minpoly :
   minpoly G F x = _root_.minpoly (fixed_points G F) x :=
-minpoly.unique' (is_integral G F x) (minpoly.irreducible G F x)
+minpoly.unique' (minpoly.irreducible G F x)
   (minpoly.eval₂ G F x) (minpoly.monic G F x)
 
 instance normal : normal (fixed_points G F) F :=

src/field_theory/minpoly.lean

@@ -290,11 +290,10 @@ by { refine minpoly.dvd K x _, rw [← is_scalar_tower.aeval_apply, minpoly.aeva
 
 variables {A x}
 
-theorem unique' [nontrivial B] {p : polynomial A} (hx : is_integral A x)
-  (hp1 : _root_.irreducible p) (hp2 : polynomial.aeval x p = 0) (hp3 : p.monic) :
-  p = minpoly A x :=
+theorem unique' [nontrivial B] {p : polynomial A} (hp1 : _root_.irreducible p)
+  (hp2 : polynomial.aeval x p = 0) (hp3 : p.monic) : p = minpoly A x :=
 let ⟨q, hq⟩ := dvd A x hp2 in
-eq_of_monic_of_associated hp3 (monic hx) $
+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
 
@@ -323,7 +322,7 @@ lemma gcd_domain_eq_field_fractions {A K R : Type*} [integral_domain A]
   [algebra A R] [is_scalar_tower A f.codomain R] {x : R} (hx : is_integral A x) :
   minpoly f.codomain x = (minpoly A x).map (localization_map.to_ring_hom f) :=
 begin
-  refine (unique' (@is_integral_of_is_scalar_tower A f.codomain R _ _ _ _ _ _ _ x hx) _ _ _).symm,
+  refine (unique' _ _ _).symm,
   { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map f
   (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
   { have htower := is_scalar_tower.aeval_apply A f.codomain R x (minpoly A x),
@@ -339,7 +338,7 @@ lemma over_int_eq_over_rat {A : Type*} [integral_domain A] {x : A} [hℚA : alge
   (hx : is_integral ℤ x) :
   minpoly ℚ x = map (int.cast_ring_hom ℚ) (minpoly ℤ x) :=
 begin
-  refine (unique' (@is_integral_of_is_scalar_tower ℤ ℚ A _ _ _ _ _ _ _ x hx) _ _ _).symm,
+  refine (unique' _ _ _).symm,
   { exact (is_primitive.int.irreducible_iff_irreducible_map_cast
   (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
   { have htower := is_scalar_tower.aeval_apply ℤ ℚ A x (minpoly ℤ x),