chore(RingTheory/{Algebraic, Localization/Integral}): rename decls to…

… use dot notation (#8437)

This PR tests a string-based tool for renaming declarations.


Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406.

This PR makes the following renames:

| From                                        | To
|

Mathlib/FieldTheory/AbelRuffini.lean

@@ -286,9 +286,9 @@ theorem isIntegral (α : solvableByRad F E) : IsIntegral F α := by
   revert α
   apply solvableByRad.induction
   · exact fun _ => isIntegral_algebraMap
-  · exact fun _ _ => isIntegral_add
-  · exact fun _ => isIntegral_neg
-  · exact fun _ _ => isIntegral_mul
+  · exact fun _ _ => IsIntegral.add
+  · exact fun _ => IsIntegral.neg
+  · exact fun _ _ => IsIntegral.mul
   · intro α hα
     exact Subalgebra.inv_mem_of_algebraic (integralClosure F (solvableByRad F E))
       (show IsAlgebraic F ↑(⟨α, hα⟩ : integralClosure F (solvableByRad F E)) from

Mathlib/FieldTheory/Adjoin.lean

@@ -1013,14 +1013,14 @@ theorem adjoin_minpoly_coeff_of_exists_primitive_element
     · exact subset_adjoin F _ (mem_frange_iff.mpr ⟨n, hn, rfl⟩)
     · exact not_mem_support_iff.mp hn ▸ zero_mem K'
   obtain ⟨p, hp⟩ := g.lifts_and_natDegree_eq_and_monic
-    g_lifts ((minpoly.monic <| isIntegral_of_finite K α).map _)
+    g_lifts ((minpoly.monic <| IsIntegral.of_finite K α).map _)
   have dvd_p : minpoly K' α ∣ p
   · apply minpoly.dvd
     rw [aeval_def, eval₂_eq_eval_map, hp.1, ← eval₂_eq_eval_map, ← aeval_def]
     exact minpoly.aeval K α
   have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α)
   · intro K
-    have := adjoin.finrank (isIntegral_of_finite K α)
+    have := adjoin.finrank (IsIntegral.of_finite K α)
     erw [adjoin_eq_top_of_adjoin_eq_top F hprim, finrank_top K E] at this
     exact this
   refine eq_of_le_of_finrank_le' hsub ?_
@@ -1030,7 +1030,7 @@ theorem adjoin_minpoly_coeff_of_exists_primitive_element
 
 theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] :
     (minpoly K x).natDegree ≤ finrank K L :=
-  le_of_eq_of_le (IntermediateField.adjoin.finrank (isIntegral_of_finite _ _)).symm
+  le_of_eq_of_le (IntermediateField.adjoin.finrank (IsIntegral.of_finite _ _)).symm
     K⟮x⟯.toSubmodule.finrank_le
 #align minpoly.nat_degree_le minpoly.natDegree_le
 

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -140,9 +140,9 @@ theorem AdjoinMonic.isIntegral (z : AdjoinMonic k) : IsIntegral k z := by
   rw [← hp]
   induction p using MvPolynomial.induction_on generalizing z with
     | h_C => exact isIntegral_algebraMap
-    | h_add _ _ ha hb => exact isIntegral_add (ha _ rfl) (hb _ rfl)
+    | h_add _ _ ha hb => exact IsIntegral.add (ha _ rfl) (hb _ rfl)
     | h_X p f ih =>
-      · refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
+      · refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
         refine ⟨f, f.2.1, ?_⟩
         erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
         exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
@@ -383,7 +383,7 @@ def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosureAux k :=
 theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosureAux k) := fun z =>
   isAlgebraic_iff_isIntegral.2 <|
     let ⟨n, x, hx⟩ := exists_ofStep k z
-    hx ▸ map_isIntegral (ofStepHom k n) (Step.isIntegral k n x)
+    hx ▸ IsIntegral.map (ofStepHom k n) (Step.isIntegral k n x)
 
 @[local instance] theorem isAlgClosure : IsAlgClosure k (AlgebraicClosureAux k) :=
   ⟨AlgebraicClosureAux.instIsAlgClosed k, isAlgebraic k⟩

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -43,7 +43,7 @@ theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x
 #align minpoly.degree_le_of_ne_zero minpoly.degree_le_of_ne_zero
 
 theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 :=
-  minpoly.ne_zero <| isIntegral_of_finite _ _
+  minpoly.ne_zero <| IsIntegral.of_finite _ _
 #align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite
 
 /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:

Mathlib/FieldTheory/Normal.lean

@@ -114,7 +114,7 @@ theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' :
   rw [normal_iff] at h ⊢
   intro x; specialize h (f.symm x)
   rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap]
-  exact ⟨map_isIntegral f h.1, splits_comp_of_splits _ _ h.2⟩
+  exact ⟨IsIntegral.map f h.1, splits_comp_of_splits _ _ h.2⟩
 #align normal.of_alg_equiv Normal.of_algEquiv
 
 theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E' :=
@@ -131,7 +131,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] :
       (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))
   refine normal_iff.mpr fun x ↦ ?_
   haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
-  have hx := isIntegral_of_finite F x
+  have hx := IsIntegral.of_finite F x
   let L := (p * minpoly F x).SplittingField
   have hL := splits_of_splits_mul' _ ?_ (SplittingField.splits (p * minpoly F x))
   · let j : E →ₐ[F] L := IsSplittingField.lift E p hL.1
@@ -218,7 +218,7 @@ def AlgHom.restrictNormalAux [h : Normal F E] :
           (minpoly.dvd E _ (by simp [aeval_algHom_apply]))
       simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
       suffices IsIntegral F _ by exact isIntegral_of_isScalarTower this
-      exact map_isIntegral ϕ (map_isIntegral (toAlgHom F E K₁) (h.isIntegral z))⟩
+      exact IsIntegral.map ϕ (IsIntegral.map (toAlgHom F E K₁) (h.isIntegral z))⟩
   map_zero' := Subtype.ext ϕ.map_zero
   map_one' := Subtype.ext ϕ.map_one
   map_add' x y := Subtype.ext (ϕ.map_add x y)

Mathlib/FieldTheory/Perfect.lean

@@ -167,7 +167,7 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K
   have hg_dvd : g.map ι ∣ (X - C a) ^ p := by
     convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
     rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
-  have ha : IsIntegral K a := isIntegral_of_finite K a
+  have ha : IsIntegral K a := IsIntegral.of_finite K a
   have hg_pow : g.map ι = (X - C a) ^ (g.map ι).natDegree := by
     obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd
     rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq,

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -324,7 +324,7 @@ theorem finite_intermediateField_of_exists_primitive_element (halg : Algebra.IsA
   -- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α` over `K`
   -- which is a monic factor of `f`
   let g : IntermediateField F E → G := fun K ↦
-    ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| isIntegral_of_finite K α).map _, by
+    ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| IsIntegral.of_finite K α).map _, by
       convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
       rw [Polynomial.map_map]; rfl⟩
   -- The map `K ↦ g` is injective

Mathlib/FieldTheory/Separable.lean

@@ -544,7 +544,7 @@ theorem isSeparable_tower_top_of_isSeparable [IsSeparable F E] : IsSeparable K E
 theorem isSeparable_tower_bot_of_isSeparable [h : IsSeparable F E] : IsSeparable F K :=
   isSeparable_iff.2 fun x => by
     refine'
-      (isSeparable_iff.1 h (algebraMap K E x)).imp isIntegral_tower_bot_of_isIntegral_field
+      (isSeparable_iff.1 h (algebraMap K E x)).imp IsIntegral.tower_bot_of_field
         fun hs => _
     obtain ⟨q, hq⟩ :=
       minpoly.dvd F x

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

@@ -129,7 +129,7 @@ def lift [Algebra K F] (f : K[X]) [IsSplittingField K L f]
 
 theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L :=
   ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
-    adjoin_rootSet L f ▸ FG_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
+    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
       if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
       else isAlgebraic_iff_isIntegral.1 ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩
 #align polynomial.is_splitting_field.finite_dimensional Polynomial.IsSplittingField.finiteDimensional

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -309,7 +309,7 @@ theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] :
     Module.Finite A B := by
   classical
   rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
-  refine' FG_adjoin_of_finite _ fun b hb => _
+  refine' fg_adjoin_of_finite _ fun b hb => _
   · simp only [mem_singleton_iff, exists_eq_left]
     have : {b : B | b ^ (n : ℕ) = 1} = (nthRoots n (1 : B)).toFinset :=
       Set.ext fun x => ⟨fun h => by simpa using h, fun h => by simpa using h⟩

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

@@ -46,9 +46,9 @@ theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) :
     fun i j => toMatrix_isIntegral H₂ _ _ _ _
   · exact hζ.isIntegral n.pos
   · refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral n.pos)
-  · exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one
+  · exact IsIntegral.sub (hζ.isIntegral n.pos) isIntegral_one
   · refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) _
-    exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one
+    exact IsIntegral.sub (hζ.isIntegral n.pos) isIntegral_one
 #align is_primitive_root.discr_zeta_eq_discr_zeta_sub_one IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one
 
 end IsPrimitiveRoot

Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

@@ -137,7 +137,7 @@ theorem powerBasis_gen_mem_adjoin_zeta_sub_one :
 @[simps!]
 noncomputable def subOnePowerBasis : PowerBasis K L :=
   (hζ.powerBasis K).ofGenMemAdjoin
-    (isIntegral_sub (IsCyclotomicExtension.integral {n} K L ζ) isIntegral_one)
+    (IsIntegral.sub (IsCyclotomicExtension.integral {n} K L ζ) isIntegral_one)
     (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)
 #align is_primitive_root.sub_one_power_basis IsPrimitiveRoot.subOnePowerBasis
 

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -82,7 +82,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExt
         (le_integralClosure_iff_isIntegral.1
           (adjoin_le_integralClosure (hζ.isIntegral (p ^ k).pos)) _)
   let B := hζ.subOnePowerBasis ℚ
-  have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.isIntegral (p ^ k).pos) isIntegral_one
+  have hint : IsIntegral ℤ B.gen := IsIntegral.sub (hζ.isIntegral (p ^ k).pos) isIntegral_one
 -- Porting note: the following `haveI` was not needed because the locale `cyclotomic` set it
 -- as instances.
   letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K

Mathlib/NumberTheory/NumberField/Norm.lean

@@ -58,7 +58,7 @@ theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x)
   replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
   refine' @isUnit_of_mul_isUnit_right (𝓞 L) _
     ⟨(univ \ {AlgEquiv.refl}).prod fun σ : L ≃ₐ[K] L => σ x,
-      prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩ _ _
+      prod_mem fun σ _ => IsIntegral.map (σ : L →+* L).toIntAlgHom x.2⟩ _ _
   convert hx using 1
   ext
   push_cast
@@ -74,7 +74,7 @@ theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L
   classical
   have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L :=
     Subalgebra.prod_mem _ fun σ _ =>
-      (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x))
+      (mem_ringOfIntegers _ _).2 (IsIntegral.map σ (RingOfIntegers.isIntegral_coe x))
   refine' ⟨⟨_, hint⟩, Subtype.ext _⟩
   rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
   simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]

Mathlib/RingTheory/Adjoin/Field.lean

@@ -67,7 +67,7 @@ theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L]
     rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
     set Ks := Algebra.adjoin F (s : Set K)
     haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
-      (FG_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
+      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
     letI := fieldOfFiniteDimensional F Ks
     letI := (f : Ks →+* L).toAlgebra
     have H5 : IsIntegral Ks a := isIntegral_of_isScalarTower H1

Mathlib/RingTheory/Adjoin/PowerBasis.lean

@@ -138,7 +138,7 @@ theorem repr_mul_isIntegral [IsDomain S] {x y : A} (hx : ∀ i, IsIntegral R (B.
   refine' IsIntegral.sum _ fun I _ => _
   simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ,
     RingHom.id_apply, Finsupp.coe_smul, Pi.smul_apply, id.smul_eq_mul]
-  refine' isIntegral_mul (hy _) (isIntegral_mul (hx _) _)
+  refine' IsIntegral.mul (hy _) (IsIntegral.mul (hx _) _)
   simp only [coe_basis, ← pow_add]
   refine' repr_gen_pow_isIntegral hB hmin _ _
 #align power_basis.repr_mul_is_integral PowerBasis.repr_mul_isIntegral
@@ -181,7 +181,7 @@ theorem toMatrix_isIntegral {B B' : PowerBasis K S} {P : R[X]} (h : aeval B.gen
   refine' IsIntegral.sum _ fun n _ => _
   rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def,
     LinearEquiv.map_smul, algebraMap_smul]
-  exact isIntegral_smul _ (repr_gen_pow_isIntegral hB hmin _ _)
+  exact IsIntegral.smul _ (repr_gen_pow_isIntegral hB hmin _ _)
 #align power_basis.to_matrix_is_integral PowerBasis.toMatrix_isIntegral
 
 end PowerBasis

Mathlib/RingTheory/Algebraic.lean

@@ -136,23 +136,23 @@ theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [Field R] [Field A]
 
 open IsScalarTower
 
-theorem isAlgebraic_algebraMap_of_isAlgebraic {a : S} :
+protected theorem IsAlgebraic.algebraMap {a : S} :
     IsAlgebraic R a → IsAlgebraic R (algebraMap S A a) := fun ⟨f, hf₁, hf₂⟩ =>
   ⟨f, hf₁, by rw [aeval_algebraMap_apply, hf₂, map_zero]⟩
-#align is_algebraic_algebra_map_of_is_algebraic isAlgebraic_algebraMap_of_isAlgebraic
+#align is_algebraic_algebra_map_of_is_algebraic IsAlgebraic.algebraMap
 
 /-- This is slightly more general than `isAlgebraic_algebraMap_of_isAlgebraic` in that it
   allows noncommutative intermediate rings `A`. -/
-theorem isAlgebraic_algHom_of_isAlgebraic {B} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A}
+protected theorem IsAlgebraic.algHom {B} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A}
     (h : IsAlgebraic R a) : IsAlgebraic R (f a) :=
   let ⟨p, hp, ha⟩ := h
   ⟨p, hp, by rw [aeval_algHom, f.comp_apply, ha, map_zero]⟩
-#align is_algebraic_alg_hom_of_is_algebraic isAlgebraic_algHom_of_isAlgebraic
+#align is_algebraic_alg_hom_of_is_algebraic IsAlgebraic.algHom
 
 /-- Transfer `Algebra.IsAlgebraic` across an `AlgEquiv`. -/
 theorem AlgEquiv.isAlgebraic {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B)
     (h : Algebra.IsAlgebraic R A) : Algebra.IsAlgebraic R B := fun b => by
-  convert← isAlgebraic_algHom_of_isAlgebraic e.toAlgHom (h _); refine e.apply_symm_apply ?_
+  convert← IsAlgebraic.algHom e.toAlgHom (h _); refine e.apply_symm_apply ?_
 #align alg_equiv.is_algebraic AlgEquiv.isAlgebraic
 
 theorem AlgEquiv.isAlgebraic_iff {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) :
@@ -163,19 +163,19 @@ theorem AlgEquiv.isAlgebraic_iff {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B)
 theorem isAlgebraic_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) :
     IsAlgebraic R (algebraMap S A a) ↔ IsAlgebraic R a :=
   ⟨fun ⟨p, hp0, hp⟩ => ⟨p, hp0, h (by rwa [map_zero, ← aeval_algebraMap_apply])⟩,
-    isAlgebraic_algebraMap_of_isAlgebraic⟩
+    IsAlgebraic.algebraMap⟩
 #align is_algebraic_algebra_map_iff isAlgebraic_algebraMap_iff
 
-theorem isAlgebraic_of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) :
+theorem IsAlgebraic.of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) :
     IsAlgebraic R r := by
   obtain ⟨p, p_nonzero, hp⟩ := ht
   refine ⟨Polynomial.expand _ n p, ?_, ?_⟩
   · rwa [Polynomial.expand_ne_zero hn]
   · rwa [Polynomial.expand_aeval n p r]
-#align is_algebraic_of_pow isAlgebraic_of_pow
+#align is_algebraic_of_pow IsAlgebraic.of_pow
 
 theorem Transcendental.pow {r : A} (ht : Transcendental R r) {n : ℕ} (hn : 0 < n) :
-    Transcendental R (r ^ n) := fun ht' => ht <| isAlgebraic_of_pow hn ht'
+    Transcendental R (r ^ n) := fun ht' => ht <| IsAlgebraic.of_pow hn ht'
 #align transcendental.pow Transcendental.pow
 
 end zero_ne_one
@@ -213,19 +213,19 @@ variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
 
 /-- If x is algebraic over R, then x is algebraic over S when S is an extension of R,
   and the map from `R` to `S` is injective. -/
-theorem isAlgebraic_of_larger_base_of_injective
+theorem IsAlgebraic.of_larger_base_of_injective
     (hinj : Function.Injective (algebraMap R S)) {x : A}
     (A_alg : IsAlgebraic R x) : IsAlgebraic S x :=
   let ⟨p, hp₁, hp₂⟩ := A_alg
   ⟨p.map (algebraMap _ _), by
     rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩
-#align is_algebraic_of_larger_base_of_injective isAlgebraic_of_larger_base_of_injective
+#align is_algebraic_of_larger_base_of_injective IsAlgebraic.of_larger_base_of_injective
 
 /-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
   and the map from `R` to `S` is injective. -/
 theorem Algebra.isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S))
     (A_alg : IsAlgebraic R A) : IsAlgebraic S A := fun x =>
-  _root_.isAlgebraic_of_larger_base_of_injective hinj (A_alg x)
+  IsAlgebraic.of_larger_base_of_injective hinj (A_alg x)
 #align algebra.is_algebraic_of_larger_base_of_injective Algebra.isAlgebraic_of_larger_base_of_injective
 
 end CommRing
@@ -239,10 +239,10 @@ variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A]
 variable (L)
 
 /-- If x is algebraic over K, then x is algebraic over L when L is an extension of K -/
-theorem isAlgebraic_of_larger_base {x : A} (A_alg : IsAlgebraic K x) :
+theorem IsAlgebraic.of_larger_base {x : A} (A_alg : IsAlgebraic K x) :
     IsAlgebraic L x :=
-  isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg
-#align is_algebraic_of_larger_base isAlgebraic_of_larger_base
+  IsAlgebraic.of_larger_base_of_injective (algebraMap K L).injective A_alg
+#align is_algebraic_of_larger_base IsAlgebraic.of_larger_base
 
 /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
 theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A :=
@@ -251,8 +251,8 @@ theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebra
 
 variable (K)
 
-theorem isAlgebraic_of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e :=
-  isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K e)
+theorem IsAlgebraic.of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e :=
+  isAlgebraic_iff_isIntegral.mpr (IsIntegral.of_finite K e)
 
 variable (A)
 

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -497,7 +497,7 @@ theorem coe_ideal_mul_inv [h : IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ 
       ← mem_one_iff] at this
   -- For that, we'll find a subalgebra that is f.g. as a module and contains `x`.
   -- `A` is a noetherian ring, so we just need to find a subalgebra between `{x}` and `I⁻¹`.
-  rw [mem_integralClosure_iff_mem_FG]
+  rw [mem_integralClosure_iff_mem_fg]
   have x_mul_mem : ∀ b ∈ (I⁻¹ : FractionalIdeal A⁰ K), x * b ∈ (I⁻¹ : FractionalIdeal A⁰ K) := by
     intro b hb
     rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI0)]