refactor(ring_theory): clean up algebraic_iff_integral (#11773)

The definitions `is_algebraic_iff_integral`, `is_algebraic_iff_integral'` and `algebra.is_algebraic_of_finite` have always been annoying me, so I decided to fix that:
 * The name `is_algebraic_iff_integral'` doesn't explain how it differs from `is_algebraic_iff_integral` (namely that the whole algebra is algebraic, rather than one element), so I renamed it to `algebra.is_algebraic_iff_integral`.
 * The two `is_algebraic_iff_integral` lemmas have an unnecessarily explicit parameter `K`, so I made that implicit
 * `is_algebraic_of_finite` has no explicit parameters (so we always have to use type ascriptions), so I made them explicit
 * Half of the usages of `is_algebraic_of_finite` are of the form `is_algebraic_iff_integral.mp is_algebraic_of_finite`, even though `is_algebraic_of_finite` is proved as `is_algebraic_iff_integral.mpr (some_proof_that_it_is_integral)`, so I split it up into a part showing it is integral, that we can use directly.

As a result, I was able to golf a few proofs.

src/field_theory/abel_ruffini.lean

@@ -285,10 +285,10 @@ begin
   { exact λ _ _, is_integral_mul },
   { exact λ α hα, subalgebra.inv_mem_of_algebraic (integral_closure F (solvable_by_rad F E))
       (show is_algebraic F ↑(⟨α, hα⟩ : integral_closure F (solvable_by_rad F E)),
-        by exact (is_algebraic_iff_is_integral F).mpr hα) },
+        by exact is_algebraic_iff_is_integral.mpr hα) },
   { intros α n hn hα,
-    obtain ⟨p, h1, h2⟩ := (is_algebraic_iff_is_integral F).mpr hα,
-    refine (is_algebraic_iff_is_integral F).mp ⟨p.comp (X ^ n),
+    obtain ⟨p, h1, h2⟩ := is_algebraic_iff_is_integral.mpr hα,
+    refine is_algebraic_iff_is_integral.mp ⟨p.comp (X ^ n),
       ⟨λ h, h1 (leading_coeff_eq_zero.mp _), by rw [aeval_comp, aeval_X_pow, h2]⟩⟩,
     rwa [←leading_coeff_eq_zero, leading_coeff_comp, leading_coeff_X_pow, one_pow, mul_one] at h,
     rwa nat_degree_X_pow }

src/field_theory/adjoin.lean

@@ -824,11 +824,9 @@ begin
       exact (S1 ⊔ S2).zero_mem },
     { obtain ⟨y, h⟩ := this.mul_inv_cancel hx',
       exact (congr_arg (∈ S1 ⊔ S2) (eq_inv_of_mul_right_eq_one (subtype.ext_iff.mp h))).mp y.2 } },
-  refine is_field_of_is_integral_of_is_field' _ (field.to_is_field K),
-  have h1 : algebra.is_algebraic K E1 := algebra.is_algebraic_of_finite,
-  have h2 : algebra.is_algebraic K E2 := algebra.is_algebraic_of_finite,
-  rw is_algebraic_iff_is_integral' at h1 h2,
-  exact is_integral_sup.mpr ⟨h1, h2⟩,
+  exact is_field_of_is_integral_of_is_field'
+    (is_integral_sup.mpr ⟨algebra.is_integral_of_finite K E1, algebra.is_integral_of_finite K E2⟩)
+    (field.to_is_field K),
 end
 
 lemma finite_dimensional_sup {K L : Type*} [field K] [field L] [algebra K L]

src/field_theory/is_alg_closed/algebraic_closure.lean

@@ -256,7 +256,7 @@ def of_step_hom (n) : step k n →ₐ[k] algebraic_closure k :=
   .. of_step k n }
 
 theorem is_algebraic : algebra.is_algebraic k (algebraic_closure k) :=
-λ z, (is_algebraic_iff_is_integral _).2 $ let ⟨n, x, hx⟩ := exists_of_step k z in
+λ z, is_algebraic_iff_is_integral.2 $ let ⟨n, x, hx⟩ := exists_of_step k z in
 hx ▸ is_integral_alg_hom (of_step_hom k n) (step.is_integral k n x)
 
 instance : is_alg_closure k (algebraic_closure k) :=

src/field_theory/is_alg_closed/basic.lean

@@ -151,7 +151,7 @@ lemma algebra_map_surjective_of_is_integral'
 lemma algebra_map_surjective_of_is_algebraic {k K : Type*} [field k] [ring K] [is_domain K]
   [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_algebraic k K) :
   function.surjective (algebra_map k K) :=
-algebra_map_surjective_of_is_integral ((is_algebraic_iff_is_integral' k).mp hf)
+algebra_map_surjective_of_is_integral (algebra.is_algebraic_iff_is_integral.mp hf)
 
 end is_alg_closed
 
@@ -265,7 +265,7 @@ begin
   letI : algebra N M := (maximal_subfield_with_hom M hL).emb.to_ring_hom.to_algebra,
   cases is_alg_closed.exists_aeval_eq_zero M (minpoly N x)
     (ne_of_gt (minpoly.degree_pos
-      ((is_algebraic_iff_is_integral _).1
+      (is_algebraic_iff_is_integral.1
         (algebra.is_algebraic_of_larger_base _ _ hL x)))) with y hy,
   let O : subalgebra N L := algebra.adjoin N {(x : L)},
   let larger_emb := ((adjoin_root.lift_hom (minpoly N x) y hy).comp

src/field_theory/polynomial_galois_group.lean

@@ -335,8 +335,7 @@ begin
     λ 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 α),
+  have hα : is_integral F α := algebra.is_integral_of_finite _ _ α,
   use finite_dimensional.finrank F⟮α⟯ p.splitting_field,
   suffices : (minpoly F α).nat_degree = p.nat_degree,
   { rw [←finite_dimensional.finrank_mul_finrank F F⟮α⟯ p.splitting_field,

src/field_theory/separable.lean

@@ -699,7 +699,7 @@ instance is_separable_self (F : Type*) [field F] : is_separable F F :=
 instance is_separable.of_finite (F K : Type*) [field F] [field K] [algebra F K]
   [finite_dimensional F K] [char_zero F] : is_separable F K :=
 have ∀ (x : K), is_integral F x,
-from λ x, (is_algebraic_iff_is_integral _).mp (algebra.is_algebraic_of_finite _),
+from λ x, algebra.is_integral_of_finite _ _ _,
 ⟨this, λ x, (minpoly.irreducible (this x)).separable⟩
 
 section is_separable_tower

src/field_theory/splitting_field.lean

@@ -909,7 +909,7 @@ if hf0 : f = 0 then (algebra.of_id K F).comp $
 alg_hom.comp (by { rw ← adjoin_roots L f, exact classical.choice (lift_of_splits _ $ λ y hy,
     have aeval y f = 0, from (eval₂_eq_eval_map _).trans $
       (mem_roots $ by exact map_ne_zero hf0).1 (multiset.mem_to_finset.mp hy),
-    ⟨(is_algebraic_iff_is_integral _).1 ⟨f, hf0, this⟩,
+    ⟨is_algebraic_iff_is_integral.1 ⟨f, hf0, this⟩,
       splits_of_splits_of_dvd _ hf0 hf $ minpoly.dvd _ _ this⟩) })
   algebra.to_top
 
@@ -918,7 +918,7 @@ theorem finite_dimensional (f : polynomial K) [is_splitting_field K L f] : finit
   fg_adjoin_of_finite (set.finite_mem_finset _) (λ y hy,
   if hf : f = 0
   then by { rw [hf, map_zero, roots_zero] at hy, cases hy }
-  else (is_algebraic_iff_is_integral _).1 ⟨f, hf, (eval₂_eq_eval_map _).trans $
+  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 K) : _root_.finite_dimensional K f.splitting_field :=

src/number_theory/class_number/finite.lean

@@ -391,7 +391,7 @@ begin
     (is_integral_closure.range_le_span_dual_basis S b hb_int),
   let bS := b.map ((linear_map.quot_ker_equiv_range _).symm ≪≫ₗ _),
   refine fintype_of_admissible_of_algebraic L bS adm
-    (λ x, (is_fraction_ring.is_algebraic_iff R K L).mpr (algebra.is_algebraic_of_finite x)),
+    (λ x, (is_fraction_ring.is_algebraic_iff R K L).mpr (algebra.is_algebraic_of_finite _ _ x)),
   { rw linear_map.ker_eq_bot.mpr,
     { exact submodule.quot_equiv_of_eq_bot _ rfl },
     { exact is_integral_closure.algebra_map_injective _ R _ } },

src/number_theory/number_field.lean

@@ -52,7 +52,7 @@ include nf
 -- See note [lower instance priority]
 attribute [priority 100, instance] number_field.to_char_zero number_field.to_finite_dimensional
 
-protected lemma is_algebraic : algebra.is_algebraic ℚ K := algebra.is_algebraic_of_finite
+protected lemma is_algebraic : algebra.is_algebraic ℚ K := algebra.is_algebraic_of_finite _ _
 
 omit nf
 

src/ring_theory/adjoin_root.lean

@@ -297,7 +297,7 @@ where `g` is a monic polynomial of degree `d`. -/
 variables [field K] {f : polynomial K}
 
 lemma is_integral_root (hf : f ≠ 0) : is_integral K (root f) :=
-(is_algebraic_iff_is_integral _).mp (is_algebraic_root hf)
+is_algebraic_iff_is_integral.mp (is_algebraic_root hf)
 
 lemma minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C (f.leading_coeff⁻¹) :=
 begin

src/ring_theory/algebraic.lean

@@ -98,7 +98,7 @@ end
 end zero_ne_one
 
 section field
-variables (K : Type u) {A : Type v} [field K] [ring A] [algebra K A]
+variables {K : Type u} {A : Type v} [field K] [ring A] [algebra K A]
 
 /-- An element of an algebra over a field is algebraic if and only if it is integral.-/
 lemma is_algebraic_iff_is_integral {x : A} :
@@ -110,10 +110,10 @@ begin
   rw [← aeval_def, alg_hom.map_mul, hpx, zero_mul],
 end
 
-lemma is_algebraic_iff_is_integral' :
+protected lemma algebra.is_algebraic_iff_is_integral :
   algebra.is_algebraic K A ↔ algebra.is_integral K A :=
-⟨λ h x, (is_algebraic_iff_is_integral K).mp (h x),
-  λ h x, (is_algebraic_iff_is_integral K).mpr (h x)⟩
+⟨λ h x, is_algebraic_iff_is_integral.mp (h x),
+  λ h x, is_algebraic_iff_is_integral.mpr (h x)⟩
 
 end field
 
@@ -158,12 +158,16 @@ _root_.is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_al
 lemma is_algebraic_of_larger_base (A_alg : is_algebraic K A) : is_algebraic L A :=
 is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_alg
 
-variables {R S K L}
+variables {R S} (K L)
+
+/-- A field extension is integral if it is finite. -/
+lemma is_integral_of_finite [finite_dimensional K L] : algebra.is_integral K L :=
+λ x, is_integral_of_submodule_noetherian ⊤
+  (is_noetherian.iff_fg.2 infer_instance) x algebra.mem_top
 
 /-- A field extension is algebraic if it is finite. -/
 lemma is_algebraic_of_finite [finite : finite_dimensional K L] : is_algebraic K L :=
-λ x, (is_algebraic_iff_is_integral _).mpr (is_integral_of_submodule_noetherian ⊤
-  (is_noetherian.iff_fg.2 infer_instance) x algebra.mem_top)
+algebra.is_algebraic_iff_is_integral.mpr (is_integral_of_finite K L)
 
 end algebra
 

src/ring_theory/dedekind_domain.lean

@@ -826,7 +826,7 @@ begin
     rintros x ⟨⟩ },
   { rintros x s hx ⟨y, hy, hs⟩,
     obtain ⟨x', y', hy', hx'⟩ := exists_integral_multiple
-      ((is_fraction_ring.is_algebraic_iff A K L).mpr (algebra.is_algebraic_of_finite x))
+      ((is_fraction_ring.is_algebraic_iff A K L).mpr (is_algebraic_of_finite _ _ x))
       ((algebra_map A L).injective_iff.mp _),
     refine ⟨y * y', mul_ne_zero hy hy', λ x'' hx'', _⟩,
     rcases finset.mem_insert.mp hx'' with (rfl | hx''),

src/ring_theory/localization.lean

@@ -2595,7 +2595,7 @@ the integral closure `C` of `A` in `L` has fraction field `L`. -/
 lemma is_fraction_ring_of_finite_extension [algebra K L] [is_scalar_tower A K L]
   [finite_dimensional K L] : is_fraction_ring C L :=
 is_fraction_ring_of_algebraic A C
-  (is_fraction_ring.comap_is_algebraic_iff.mpr (is_algebraic_of_finite : is_algebraic K L))
+  (is_fraction_ring.comap_is_algebraic_iff.mpr (is_algebraic_of_finite K L))
   (λ x hx, is_fraction_ring.to_map_eq_zero_iff.mp ((algebra_map K L).map_eq_zero.mp $
     (is_scalar_tower.algebra_map_apply _ _ _ _).symm.trans hx))