feat(RingTheory/IntegralClosure): prove Module.Finite R (adjoin R S) for finite set S of integral elements (#20970)

Prove that `Algebra.adjoin R S` has finite rank over `R` when `S` is finite with elements that are all integral over `R`.
Special case for singleton included.

Author: mistarro

Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

@@ -201,6 +201,14 @@ theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsI
           (his a <| Set.mem_insert a s).fg_adjoin_singleton)
     his
 
+theorem Algebra.finite_adjoin_of_finite_of_isIntegral {s : Set A} (hf : s.Finite)
+    (hi : ∀ x ∈ s, IsIntegral R x) : Module.Finite R (adjoin R s) :=
+  Module.Finite.iff_fg.mpr <| fg_adjoin_of_finite hf hi
+
+theorem Algebra.finite_adjoin_simple_of_isIntegral {x : A} (hi : IsIntegral R x) :
+    Module.Finite R (adjoin R {x}) :=
+  Module.Finite.iff_fg.mpr hi.fg_adjoin_singleton
+
 theorem isNoetherian_adjoin_finset [IsNoetherianRing R] (s : Finset A)
     (hs : ∀ x ∈ s, IsIntegral R x) : IsNoetherian R (Algebra.adjoin R (s : Set A)) :=
   isNoetherian_of_fg_of_noetherian _ (fg_adjoin_of_finite s.finite_toSet hs)

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

@@ -132,7 +132,7 @@ theorem le_integralClosure_iff_isIntegral {S : Subalgebra R A} :
       Algebra.isIntegral_def.symm
 
 theorem Algebra.IsIntegral.adjoin {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) :
-    Algebra.IsIntegral R (Algebra.adjoin R S) :=
+    Algebra.IsIntegral R (adjoin R S) :=
   le_integralClosure_iff_isIntegral.mp <| adjoin_le hS
 
 theorem integralClosure_eq_top_iff : integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A := by