diff --git a/Mathlib.lean b/Mathlib.lean
index 0b2ba3cf05fec..6b05b7422f10f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1762,7 +1762,7 @@ import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RingTheory.Adjoin.Basic
-import Mathlib.RingTheory.Adjoin.Fg
+import Mathlib.RingTheory.Adjoin.FG
 import Mathlib.RingTheory.Adjoin.Tower
 import Mathlib.RingTheory.AlgebraTower
 import Mathlib.RingTheory.ChainOfDivisors
@@ -1779,7 +1779,7 @@ import Mathlib.RingTheory.Flat
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Ideal.IdempotentFg
+import Mathlib.RingTheory.Ideal.IdempotentFG
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient
diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean
index 3758d14fe9dd1..4b75a51bb363e 100644
--- a/Mathlib/GroupTheory/Abelianization.lean
+++ b/Mathlib/GroupTheory/Abelianization.lean
@@ -59,7 +59,7 @@ instance commutator_characteristic : (commutator G).Characteristic :=
   Subgroup.commutator_characteristic ⊤ ⊤
 #align commutator_characteristic commutator_characteristic
 
-instance [Finite (commutatorSet G)] : Group.Fg (commutator G) := by
+instance [Finite (commutatorSet G)] : Group.FG (commutator G) := by
   rw [commutator_eq_closure]
   apply Group.closure_finite_fg
 
@@ -276,7 +276,7 @@ def closureCommutatorRepresentatives : Subgroup G :=
 #align closure_commutator_representatives closureCommutatorRepresentatives
 
 instance closureCommutatorRepresentatives_fg [Finite (commutatorSet G)] :
-    Group.Fg (closureCommutatorRepresentatives G) :=
+    Group.FG (closureCommutatorRepresentatives G) :=
   Group.closure_finite_fg _
 #align closure_commutator_representatives_fg closureCommutatorRepresentatives_fg
 
diff --git a/Mathlib/GroupTheory/Finiteness.lean b/Mathlib/GroupTheory/Finiteness.lean
index 91b2a3e961096..d6a516ff9084f 100644
--- a/Mathlib/GroupTheory/Finiteness.lean
+++ b/Mathlib/GroupTheory/Finiteness.lean
@@ -18,16 +18,16 @@ import Mathlib.Data.Finset.Preimage
 /-!
 # Finitely generated monoids and groups
 
-We define finitely generated monoids and groups. See also `Submodule.Fg` and `Module.Finite` for
+We define finitely generated monoids and groups. See also `Submodule.FG` and `Module.Finite` for
 finitely-generated modules.
 
 ## Main definition
 
-* `Submonoid.Fg S`, `AddSubmonoid.Fg S` : A submonoid `S` is finitely generated.
-* `Monoid.Fg M`, `AddMonoid.Fg M` : A typeclass indicating a type `M` is finitely generated as a
+* `Submonoid.FG S`, `AddSubmonoid.FG S` : A submonoid `S` is finitely generated.
+* `Monoid.FG M`, `AddMonoid.FG M` : A typeclass indicating a type `M` is finitely generated as a
 monoid.
-* `Subgroup.Fg S`, `AddSubgroup.Fg S` : A subgroup `S` is finitely generated.
-* `Group.Fg M`, `AddGroup.Fg M` : A typeclass indicating a type `M` is finitely generated as a
+* `Subgroup.FG S`, `AddSubgroup.FG S` : A subgroup `S` is finitely generated.
+* `Group.FG M`, `AddGroup.FG M` : A typeclass indicating a type `M` is finitely generated as a
 group.
 
 -/
@@ -44,26 +44,26 @@ section Submonoid
 
 /-- A submonoid of `M` is finitely generated if it is the closure of a finite subset of `M`. -/
 @[to_additive]
-def Submonoid.Fg (P : Submonoid M) : Prop :=
+def Submonoid.FG (P : Submonoid M) : Prop :=
   ∃ S : Finset M, Submonoid.closure ↑S = P
-#align submonoid.fg Submonoid.Fg
-#align add_submonoid.fg AddSubmonoid.Fg
+#align submonoid.fg Submonoid.FG
+#align add_submonoid.fg AddSubmonoid.FG
 
 /-- An additive submonoid of `N` is finitely generated if it is the closure of a finite subset of
 `M`. -/
-add_decl_doc AddSubmonoid.Fg
+add_decl_doc AddSubmonoid.FG
 
-/-- An equivalent expression of `Submonoid.Fg` in terms of `Set.Finite` instead of `Finset`. -/
-@[to_additive "An equivalent expression of `AddSubmonoid.Fg` in terms of `Set.Finite` instead of
+/-- An equivalent expression of `Submonoid.FG` in terms of `Set.Finite` instead of `Finset`. -/
+@[to_additive "An equivalent expression of `AddSubmonoid.FG` in terms of `Set.Finite` instead of
 `Finset`."]
 theorem Submonoid.fg_iff (P : Submonoid M) :
-    Submonoid.Fg P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
+    Submonoid.FG P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
   ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
     ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩
 #align submonoid.fg_iff Submonoid.fg_iff
 #align add_submonoid.fg_iff AddSubmonoid.fg_iff
 
-theorem Submonoid.fg_iff_add_fg (P : Submonoid M) : P.Fg ↔ P.toAddSubmonoid.Fg :=
+theorem Submonoid.fg_iff_add_fg (P : Submonoid M) : P.FG ↔ P.toAddSubmonoid.FG :=
   ⟨fun h =>
     let ⟨S, hS, hf⟩ := (Submonoid.fg_iff _).1 h
     (AddSubmonoid.fg_iff _).mpr
@@ -74,7 +74,7 @@ theorem Submonoid.fg_iff_add_fg (P : Submonoid M) : P.Fg ↔ P.toAddSubmonoid.Fg
       ⟨Multiplicative.ofAdd ⁻¹' T, by simp [← AddSubmonoid.toSubmonoid'_closure, hT], hf⟩⟩
 #align submonoid.fg_iff_add_fg Submonoid.fg_iff_add_fg
 
-theorem AddSubmonoid.fg_iff_mul_fg (P : AddSubmonoid N) : P.Fg ↔ P.toSubmonoid.Fg := by
+theorem AddSubmonoid.fg_iff_mul_fg (P : AddSubmonoid N) : P.FG ↔ P.toSubmonoid.FG := by
   convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm
 #align add_submonoid.fg_iff_mul_fg AddSubmonoid.fg_iff_mul_fg
 
@@ -85,56 +85,56 @@ section Monoid
 variable (M N)
 
 /-- A monoid is finitely generated if it is finitely generated as a submonoid of itself. -/
-class Monoid.Fg : Prop where
-  out : (⊤ : Submonoid M).Fg
-#align monoid.fg Monoid.Fg
+class Monoid.FG : Prop where
+  out : (⊤ : Submonoid M).FG
+#align monoid.fg Monoid.FG
 
 /-- An additive monoid is finitely generated if it is finitely generated as an additive submonoid of
 itself. -/
-class AddMonoid.Fg : Prop where
-  out : (⊤ : AddSubmonoid N).Fg
-#align add_monoid.fg AddMonoid.Fg
+class AddMonoid.FG : Prop where
+  out : (⊤ : AddSubmonoid N).FG
+#align add_monoid.fg AddMonoid.FG
 
-attribute [to_additive] Monoid.Fg
+attribute [to_additive] Monoid.FG
 
 variable {M N}
 
-theorem Monoid.fg_def : Monoid.Fg M ↔ (⊤ : Submonoid M).Fg :=
+theorem Monoid.fg_def : Monoid.FG M ↔ (⊤ : Submonoid M).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align monoid.fg_def Monoid.fg_def
 
-theorem AddMonoid.fg_def : AddMonoid.Fg N ↔ (⊤ : AddSubmonoid N).Fg :=
+theorem AddMonoid.fg_def : AddMonoid.FG N ↔ (⊤ : AddSubmonoid N).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align add_monoid.fg_def AddMonoid.fg_def
 
-/-- An equivalent expression of `Monoid.Fg` in terms of `Set.Finite` instead of `Finset`. -/
+/-- An equivalent expression of `Monoid.FG` in terms of `Set.Finite` instead of `Finset`. -/
 @[to_additive
-      "An equivalent expression of `AddMonoid.Fg` in terms of `Set.Finite` instead of `Finset`."]
+      "An equivalent expression of `AddMonoid.FG` in terms of `Set.Finite` instead of `Finset`."]
 theorem Monoid.fg_iff :
-    Monoid.Fg M ↔ ∃ S : Set M, Submonoid.closure S = (⊤ : Submonoid M) ∧ S.Finite :=
+    Monoid.FG M ↔ ∃ S : Set M, Submonoid.closure S = (⊤ : Submonoid M) ∧ S.Finite :=
   ⟨fun h => (Submonoid.fg_iff ⊤).1 h.out, fun h => ⟨(Submonoid.fg_iff ⊤).2 h⟩⟩
 #align monoid.fg_iff Monoid.fg_iff
 #align add_monoid.fg_iff AddMonoid.fg_iff
 
-theorem Monoid.fg_iff_add_fg : Monoid.Fg M ↔ AddMonoid.Fg (Additive M) :=
+theorem Monoid.fg_iff_add_fg : Monoid.FG M ↔ AddMonoid.FG (Additive M) :=
   ⟨fun h => ⟨(Submonoid.fg_iff_add_fg ⊤).1 h.out⟩, fun h => ⟨(Submonoid.fg_iff_add_fg ⊤).2 h.out⟩⟩
 #align monoid.fg_iff_add_fg Monoid.fg_iff_add_fg
 
-theorem AddMonoid.fg_iff_mul_fg : AddMonoid.Fg N ↔ Monoid.Fg (Multiplicative N) :=
+theorem AddMonoid.fg_iff_mul_fg : AddMonoid.FG N ↔ Monoid.FG (Multiplicative N) :=
   ⟨fun h => ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).1 h.out⟩, fun h =>
     ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).2 h.out⟩⟩
 #align add_monoid.fg_iff_mul_fg AddMonoid.fg_iff_mul_fg
 
-instance AddMonoid.fg_of_monoid_fg [Monoid.Fg M] : AddMonoid.Fg (Additive M) :=
+instance AddMonoid.fg_of_monoid_fg [Monoid.FG M] : AddMonoid.FG (Additive M) :=
   Monoid.fg_iff_add_fg.1 ‹_›
 #align add_monoid.fg_of_monoid_fg AddMonoid.fg_of_monoid_fg
 
-instance Monoid.fg_of_addMonoid_fg [AddMonoid.Fg N] : Monoid.Fg (Multiplicative N) :=
+instance Monoid.fg_of_addMonoid_fg [AddMonoid.FG N] : Monoid.FG (Multiplicative N) :=
   AddMonoid.fg_iff_mul_fg.1 ‹_›
 #align monoid.fg_of_add_monoid_fg Monoid.fg_of_addMonoid_fg
 
 @[to_additive]
-instance (priority := 100) Monoid.fg_of_finite [Finite M] : Monoid.Fg M := by
+instance (priority := 100) Monoid.fg_of_finite [Finite M] : Monoid.FG M := by
   cases nonempty_fintype M
   exact ⟨⟨Finset.univ, by rw [Finset.coe_univ] ; exact Submonoid.closure_univ⟩⟩
 #align monoid.fg_of_finite Monoid.fg_of_finite
@@ -143,17 +143,17 @@ instance (priority := 100) Monoid.fg_of_finite [Finite M] : Monoid.Fg M := by
 end Monoid
 
 @[to_additive]
-theorem Submonoid.Fg.map {M' : Type _} [Monoid M'] {P : Submonoid M} (h : P.Fg) (e : M →* M') :
-    (P.map e).Fg := by
+theorem Submonoid.FG.map {M' : Type _} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') :
+    (P.map e).FG := by
   classical
     obtain ⟨s, rfl⟩ := h
     exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
-#align submonoid.fg.map Submonoid.Fg.map
-#align add_submonoid.fg.map AddSubmonoid.Fg.map
+#align submonoid.fg.map Submonoid.FG.map
+#align add_submonoid.fg.map AddSubmonoid.FG.map
 
 @[to_additive]
-theorem Submonoid.Fg.map_injective {M' : Type _} [Monoid M'] {P : Submonoid M} (e : M →* M')
-    (he : Function.Injective e) (h : (P.map e).Fg) : P.Fg := by
+theorem Submonoid.FG.map_injective {M' : Type _} [Monoid M'] {P : Submonoid M} (e : M →* M')
+    (he : Function.Injective e) (h : (P.map e).FG) : P.FG := by
   obtain ⟨s, hs⟩ := h
   use s.preimage e (he.injOn _)
   apply Submonoid.map_injective_of_injective he
@@ -162,19 +162,19 @@ theorem Submonoid.Fg.map_injective {M' : Type _} [Monoid M'] {P : Submonoid M} (
   rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
       MonoidHom.mrange_eq_map e]
   exact Submonoid.monotone_map le_top
-#align submonoid.fg.map_injective Submonoid.Fg.map_injective
-#align add_submonoid.fg.map_injective AddSubmonoid.Fg.map_injective
+#align submonoid.fg.map_injective Submonoid.FG.map_injective
+#align add_submonoid.fg.map_injective AddSubmonoid.FG.map_injective
 
 @[to_additive (attr := simp)]
-theorem Monoid.fg_iff_submonoid_fg (N : Submonoid M) : Monoid.Fg N ↔ N.Fg := by
+theorem Monoid.fg_iff_submonoid_fg (N : Submonoid M) : Monoid.FG N ↔ N.FG := by
   conv_rhs => rw [← N.range_subtype, MonoidHom.mrange_eq_map]
   exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩
 #align monoid.fg_iff_submonoid_fg Monoid.fg_iff_submonoid_fg
 #align add_monoid.fg_iff_add_submonoid_fg AddMonoid.fg_iff_addSubmonoid_fg
 
 @[to_additive]
-theorem Monoid.fg_of_surjective {M' : Type _} [Monoid M'] [Monoid.Fg M] (f : M →* M')
-    (hf : Function.Surjective f) : Monoid.Fg M' := by
+theorem Monoid.fg_of_surjective {M' : Type _} [Monoid M'] [Monoid.FG M] (f : M →* M')
+    (hf : Function.Surjective f) : Monoid.FG M' := by
   classical
     obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
     use s.image f
@@ -184,33 +184,33 @@ theorem Monoid.fg_of_surjective {M' : Type _} [Monoid M'] [Monoid.Fg M] (f : M 
 #align add_monoid.fg_of_surjective AddMonoid.fg_of_surjective
 
 @[to_additive]
-instance Monoid.fg_range {M' : Type _} [Monoid M'] [Monoid.Fg M] (f : M →* M') :
-    Monoid.Fg (MonoidHom.mrange f) :=
+instance Monoid.fg_range {M' : Type _} [Monoid M'] [Monoid.FG M] (f : M →* M') :
+    Monoid.FG (MonoidHom.mrange f) :=
   Monoid.fg_of_surjective f.mrangeRestrict f.mrangeRestrict_surjective
 #align monoid.fg_range Monoid.fg_range
 #align add_monoid.fg_range AddMonoid.fg_range
 
 @[to_additive AddSubmonoid.multiples_fg]
-theorem Submonoid.powers_fg (r : M) : (Submonoid.powers r).Fg :=
+theorem Submonoid.powers_fg (r : M) : (Submonoid.powers r).FG :=
   ⟨{r}, (Finset.coe_singleton r).symm ▸ (Submonoid.powers_eq_closure r).symm⟩
 #align submonoid.powers_fg Submonoid.powers_fg
 #align add_submonoid.multiples_fg AddSubmonoid.multiples_fg
 
 @[to_additive AddMonoid.multiples_fg]
-instance Monoid.powers_fg (r : M) : Monoid.Fg (Submonoid.powers r) :=
+instance Monoid.powers_fg (r : M) : Monoid.FG (Submonoid.powers r) :=
   (Monoid.fg_iff_submonoid_fg _).mpr (Submonoid.powers_fg r)
 #align monoid.powers_fg Monoid.powers_fg
 #align add_monoid.multiples_fg AddMonoid.multiples_fg
 
 @[to_additive]
-instance Monoid.closure_finset_fg (s : Finset M) : Monoid.Fg (Submonoid.closure (s : Set M)) := by
+instance Monoid.closure_finset_fg (s : Finset M) : Monoid.FG (Submonoid.closure (s : Set M)) := by
   refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
   rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]
 #align monoid.closure_finset_fg Monoid.closure_finset_fg
 #align add_monoid.closure_finset_fg AddMonoid.closure_finset_fg
 
 @[to_additive]
-instance Monoid.closure_finite_fg (s : Set M) [Finite s] : Monoid.Fg (Submonoid.closure s) :=
+instance Monoid.closure_finite_fg (s : Set M) [Finite s] : Monoid.FG (Submonoid.closure s) :=
   haveI := Fintype.ofFinite s
   s.coe_toFinset ▸ Monoid.closure_finset_fg s.toFinset
 #align monoid.closure_finite_fg Monoid.closure_finite_fg
@@ -225,20 +225,20 @@ section Subgroup
 
 /-- A subgroup of `G` is finitely generated if it is the closure of a finite subset of `G`. -/
 @[to_additive]
-def Subgroup.Fg (P : Subgroup G) : Prop :=
+def Subgroup.FG (P : Subgroup G) : Prop :=
   ∃ S : Finset G, Subgroup.closure ↑S = P
-#align subgroup.fg Subgroup.Fg
-#align add_subgroup.fg AddSubgroup.Fg
+#align subgroup.fg Subgroup.FG
+#align add_subgroup.fg AddSubgroup.FG
 
 /-- An additive subgroup of `H` is finitely generated if it is the closure of a finite subset of
 `H`. -/
-add_decl_doc AddSubgroup.Fg
+add_decl_doc AddSubgroup.FG
 
-/-- An equivalent expression of `Subgroup.Fg` in terms of `Set.Finite` instead of `Finset`. -/
+/-- An equivalent expression of `Subgroup.FG` in terms of `Set.Finite` instead of `Finset`. -/
 @[to_additive "An equivalent expression of `AddSubgroup.fg` in terms of `Set.Finite` instead of
 `Finset`."]
 theorem Subgroup.fg_iff (P : Subgroup G) :
-    Subgroup.Fg P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite :=
+    Subgroup.FG P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite :=
   ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
     ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩
 #align subgroup.fg_iff Subgroup.fg_iff
@@ -247,7 +247,7 @@ theorem Subgroup.fg_iff (P : Subgroup G) :
 /-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid. -/
 @[to_additive "An additive subgroup is finitely generated if
 and only if it is finitely generated as an additive submonoid."]
-theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.Fg ↔ P.toSubmonoid.Fg := by
+theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.FG ↔ P.toSubmonoid.FG := by
   constructor
   · rintro ⟨S, rfl⟩
     rw [Submonoid.fg_iff]
@@ -262,12 +262,12 @@ theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.Fg ↔ P.toSubmonoid.F
 #align subgroup.fg_iff_submonoid_fg Subgroup.fg_iff_submonoid_fg
 #align add_subgroup.fg_iff_add_submonoid.fg AddSubgroup.fg_iff_addSubmonoid_fg
 
-theorem Subgroup.fg_iff_add_fg (P : Subgroup G) : P.Fg ↔ P.toAddSubgroup.Fg := by
+theorem Subgroup.fg_iff_add_fg (P : Subgroup G) : P.FG ↔ P.toAddSubgroup.FG := by
   rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
   exact (Subgroup.toSubmonoid P).fg_iff_add_fg
 #align subgroup.fg_iff_add_fg Subgroup.fg_iff_add_fg
 
-theorem AddSubgroup.fg_iff_mul_fg (P : AddSubgroup H) : P.Fg ↔ P.toSubgroup.Fg := by
+theorem AddSubgroup.fg_iff_mul_fg (P : AddSubgroup H) : P.FG ↔ P.toSubgroup.FG := by
   rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
   exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)
 #align add_subgroup.fg_iff_mul_fg AddSubgroup.fg_iff_mul_fg
@@ -279,39 +279,39 @@ section Group
 variable (G H)
 
 /-- A group is finitely generated if it is finitely generated as a submonoid of itself. -/
-class Group.Fg : Prop where
-  out : (⊤ : Subgroup G).Fg
-#align group.fg Group.Fg
+class Group.FG : Prop where
+  out : (⊤ : Subgroup G).FG
+#align group.fg Group.FG
 
 /-- An additive group is finitely generated if it is finitely generated as an additive submonoid of
 itself. -/
-class AddGroup.Fg : Prop where
-  out : (⊤ : AddSubgroup H).Fg
-#align add_group.fg AddGroup.Fg
+class AddGroup.FG : Prop where
+  out : (⊤ : AddSubgroup H).FG
+#align add_group.fg AddGroup.FG
 
-attribute [to_additive] Group.Fg
+attribute [to_additive] Group.FG
 
 variable {G H}
 
-theorem Group.fg_def : Group.Fg G ↔ (⊤ : Subgroup G).Fg :=
+theorem Group.fg_def : Group.FG G ↔ (⊤ : Subgroup G).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align group.fg_def Group.fg_def
 
-theorem AddGroup.fg_def : AddGroup.Fg H ↔ (⊤ : AddSubgroup H).Fg :=
+theorem AddGroup.fg_def : AddGroup.FG H ↔ (⊤ : AddSubgroup H).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align add_group.fg_def AddGroup.fg_def
 
-/-- An equivalent expression of `Group.Fg` in terms of `Set.Finite` instead of `Finset`. -/
+/-- An equivalent expression of `Group.FG` in terms of `Set.Finite` instead of `Finset`. -/
 @[to_additive
       "An equivalent expression of `AddGroup.fg` in terms of `Set.Finite` instead of `Finset`."]
-theorem Group.fg_iff : Group.Fg G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite :=
+theorem Group.fg_iff : Group.FG G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite :=
   ⟨fun h => (Subgroup.fg_iff ⊤).1 h.out, fun h => ⟨(Subgroup.fg_iff ⊤).2 h⟩⟩
 #align group.fg_iff Group.fg_iff
 #align add_group.fg_iff AddGroup.fg_iff
 
 @[to_additive]
 theorem Group.fg_iff' :
-    Group.Fg G ↔ ∃ (n : _)(S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤ :=
+    Group.FG G ↔ ∃ (n : _)(S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤ :=
   Group.fg_def.trans ⟨fun ⟨S, hS⟩ => ⟨S.card, S, rfl, hS⟩, fun ⟨_n, S, _hn, hS⟩ => ⟨S, hS⟩⟩
 #align group.fg_iff' Group.fg_iff'
 #align add_group.fg_iff' AddGroup.fg_iff'
@@ -319,59 +319,59 @@ theorem Group.fg_iff' :
 /-- A group is finitely generated if and only if it is finitely generated as a monoid. -/
 @[to_additive "An additive group is finitely generated if and only
 if it is finitely generated as an additive monoid."]
-theorem Group.fg_iff_monoid_fg : Group.Fg G ↔ Monoid.Fg G :=
+theorem Group.fg_iff_monoid_fg : Group.FG G ↔ Monoid.FG G :=
   ⟨fun h => Monoid.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).1 (Group.fg_def.1 h), fun h =>
     Group.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).2 (Monoid.fg_def.1 h)⟩
 #align group.fg_iff_monoid.fg Group.fg_iff_monoid_fg
 #align add_group.fg_iff_add_monoid.fg AddGroup.fg_iff_addMonoid_fg
 
-theorem GroupFg.iff_add_fg : Group.Fg G ↔ AddGroup.Fg (Additive G) :=
+theorem GroupFG.iff_add_fg : Group.FG G ↔ AddGroup.FG (Additive G) :=
   ⟨fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).1 h.out⟩, fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).2 h.out⟩⟩
-#align group_fg.iff_add_fg GroupFg.iff_add_fg
+#align group_fg.iff_add_fg GroupFG.iff_add_fg
 
-theorem AddGroup.fg_iff_mul_fg : AddGroup.Fg H ↔ Group.Fg (Multiplicative H) :=
+theorem AddGroup.fg_iff_mul_fg : AddGroup.FG H ↔ Group.FG (Multiplicative H) :=
   ⟨fun h => ⟨(AddSubgroup.fg_iff_mul_fg ⊤).1 h.out⟩, fun h =>
     ⟨(AddSubgroup.fg_iff_mul_fg ⊤).2 h.out⟩⟩
 #align add_group.fg_iff_mul_fg AddGroup.fg_iff_mul_fg
 
-instance AddGroup.fg_of_group_fg [Group.Fg G] : AddGroup.Fg (Additive G) :=
-  GroupFg.iff_add_fg.1 ‹_›
+instance AddGroup.fg_of_group_fg [Group.FG G] : AddGroup.FG (Additive G) :=
+  GroupFG.iff_add_fg.1 ‹_›
 #align add_group.fg_of_group_fg AddGroup.fg_of_group_fg
 
-instance Group.fg_of_mul_group_fg [AddGroup.Fg H] : Group.Fg (Multiplicative H) :=
+instance Group.fg_of_mul_group_fg [AddGroup.FG H] : Group.FG (Multiplicative H) :=
   AddGroup.fg_iff_mul_fg.1 ‹_›
 #align group.fg_of_mul_group_fg Group.fg_of_mul_group_fg
 
 @[to_additive]
-instance (priority := 100) Group.fg_of_finite [Finite G] : Group.Fg G := by
+instance (priority := 100) Group.fg_of_finite [Finite G] : Group.FG G := by
   cases nonempty_fintype G
   exact ⟨⟨Finset.univ, by rw [Finset.coe_univ] ; exact Subgroup.closure_univ⟩⟩
 #align group.fg_of_finite Group.fg_of_finite
 #align add_group.fg_of_finite AddGroup.fg_of_finite
 
 @[to_additive]
-theorem Group.fg_of_surjective {G' : Type _} [Group G'] [hG : Group.Fg G] {f : G →* G'}
-    (hf : Function.Surjective f) : Group.Fg G' :=
+theorem Group.fg_of_surjective {G' : Type _} [Group G'] [hG : Group.FG G] {f : G →* G'}
+    (hf : Function.Surjective f) : Group.FG G' :=
   Group.fg_iff_monoid_fg.mpr <|
     @Monoid.fg_of_surjective G _ G' _ (Group.fg_iff_monoid_fg.mp hG) f hf
 #align group.fg_of_surjective Group.fg_of_surjective
 #align add_group.fg_of_surjective AddGroup.fg_of_surjective
 
 @[to_additive]
-instance Group.fg_range {G' : Type _} [Group G'] [Group.Fg G] (f : G →* G') : Group.Fg f.range :=
+instance Group.fg_range {G' : Type _} [Group G'] [Group.FG G] (f : G →* G') : Group.FG f.range :=
   Group.fg_of_surjective f.rangeRestrict_surjective
 #align group.fg_range Group.fg_range
 #align add_group.fg_range AddGroup.fg_range
 
 @[to_additive]
-instance Group.closure_finset_fg (s : Finset G) : Group.Fg (Subgroup.closure (s : Set G)) := by
+instance Group.closure_finset_fg (s : Finset G) : Group.FG (Subgroup.closure (s : Set G)) := by
   refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
   rw [Finset.coe_preimage, ← Subgroup.coeSubtype, Subgroup.closure_preimage_eq_top]
 #align group.closure_finset_fg Group.closure_finset_fg
 #align add_group.closure_finset_fg AddGroup.closure_finset_fg
 
 @[to_additive]
-instance Group.closure_finite_fg (s : Set G) [Finite s] : Group.Fg (Subgroup.closure s) :=
+instance Group.closure_finite_fg (s : Set G) [Finite s] : Group.FG (Subgroup.closure s) :=
   haveI := Fintype.ofFinite s
   s.coe_toFinset ▸ Group.closure_finset_fg s.toFinset
 #align group.closure_finite_fg Group.closure_finite_fg
@@ -381,20 +381,20 @@ variable (G)
 
 /-- The minimum number of generators of a group. -/
 @[to_additive "The minimum number of generators of an additive group"]
-noncomputable def Group.rank [h : Group.Fg G] :=
+noncomputable def Group.rank [h : Group.FG G] :=
   @Nat.find _ (Classical.decPred _) (Group.fg_iff'.mp h)
 #align group.rank Group.rank
 #align add_group.rank AddGroup.rank
 
 @[to_additive]
-theorem Group.rank_spec [h : Group.Fg G] :
+theorem Group.rank_spec [h : Group.FG G] :
     ∃ S : Finset G, S.card = Group.rank G ∧ Subgroup.closure (S : Set G) = ⊤ :=
   @Nat.find_spec _ (Classical.decPred _) (Group.fg_iff'.mp h)
 #align group.rank_spec Group.rank_spec
 #align add_group.rank_spec AddGroup.rank_spec
 
 @[to_additive]
-theorem Group.rank_le [h : Group.Fg G] {S : Finset G} (hS : Subgroup.closure (S : Set G) = ⊤) :
+theorem Group.rank_le [h : Group.FG G] {S : Finset G} (hS : Subgroup.closure (S : Set G) = ⊤) :
     Group.rank G ≤ S.card :=
   @Nat.find_le _ _ (Classical.decPred _) (Group.fg_iff'.mp h) ⟨S, rfl, hS⟩
 #align group.rank_le Group.rank_le
@@ -403,7 +403,7 @@ theorem Group.rank_le [h : Group.Fg G] {S : Finset G} (hS : Subgroup.closure (S
 variable {G} {G' : Type _} [Group G']
 
 @[to_additive]
-theorem Group.rank_le_of_surjective [Group.Fg G] [Group.Fg G'] (f : G →* G')
+theorem Group.rank_le_of_surjective [Group.FG G] [Group.FG G'] (f : G →* G')
     (hf : Function.Surjective f) : Group.rank G' ≤ Group.rank G := by
   classical
     obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
@@ -415,13 +415,13 @@ theorem Group.rank_le_of_surjective [Group.Fg G] [Group.Fg G'] (f : G →* G')
 #align add_group.rank_le_of_surjective AddGroup.rank_le_of_surjective
 
 @[to_additive]
-theorem Group.rank_range_le [Group.Fg G] {f : G →* G'} : Group.rank f.range ≤ Group.rank G :=
+theorem Group.rank_range_le [Group.FG G] {f : G →* G'} : Group.rank f.range ≤ Group.rank G :=
   Group.rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective
 #align group.rank_range_le Group.rank_range_le
 #align add_group.rank_range_le AddGroup.rank_range_le
 
 @[to_additive]
-theorem Group.rank_congr [Group.Fg G] [Group.Fg G'] (f : G ≃* G') : Group.rank G = Group.rank G' :=
+theorem Group.rank_congr [Group.FG G] [Group.FG G'] (f : G ≃* G') : Group.rank G = Group.rank G' :=
   le_antisymm (Group.rank_le_of_surjective f.symm f.symm.surjective)
     (Group.rank_le_of_surjective f f.surjective)
 #align group.rank_congr Group.rank_congr
@@ -432,7 +432,7 @@ end Group
 namespace Subgroup
 
 @[to_additive]
-theorem rank_congr {H K : Subgroup G} [Group.Fg H] [Group.Fg K] (h : H = K) :
+theorem rank_congr {H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) :
     Group.rank H = Group.rank K := by subst h; rfl
 #align subgroup.rank_congr Subgroup.rank_congr
 #align add_subgroup.rank_congr AddSubgroup.rank_congr
@@ -466,7 +466,7 @@ end Subgroup
 section QuotientGroup
 
 @[to_additive]
-instance QuotientGroup.fg [Group.Fg G] (N : Subgroup G) [Subgroup.Normal N] : Group.Fg <| G ⧸ N :=
+instance QuotientGroup.fg [Group.FG G] (N : Subgroup G) [Subgroup.Normal N] : Group.FG <| G ⧸ N :=
   Group.fg_of_surjective <| QuotientGroup.mk'_surjective N
 #align quotient_group.fg QuotientGroup.fg
 #align quotient_add_group.fg QuotientAddGroup.fg
diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
index c45e33cdd2316..fa25770fcbd6a 100644
--- a/Mathlib/GroupTheory/Index.lean
+++ b/Mathlib/GroupTheory/Index.lean
@@ -602,12 +602,12 @@ instance finiteIndex_normalCore [H.FiniteIndex] : H.normalCore.FiniteIndex := by
 
 variable (G)
 
-instance finiteIndex_center [Finite (commutatorSet G)] [Group.Fg G] : FiniteIndex (center G) := by
+instance finiteIndex_center [Finite (commutatorSet G)] [Group.FG G] : FiniteIndex (center G) := by
   obtain ⟨S, -, hS⟩ := Group.rank_spec G
   exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
 #align subgroup.finite_index_center Subgroup.finiteIndex_center
 
-theorem index_center_le_pow [Finite (commutatorSet G)] [Group.Fg G] :
+theorem index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] :
     (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G := by
   obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
   rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
index 21cf5ba4ea681..f3bb85e81c34e 100644
--- a/Mathlib/LinearAlgebra/FiniteDimensional.lean
+++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -705,7 +705,7 @@ section DivisionRing
 variable [DivisionRing K] [AddCommGroup V] [Module K V]
 
 /-- A submodule is finitely generated if and only if it is finite-dimensional -/
-theorem fg_iff_finiteDimensional (s : Submodule K V) : s.Fg ↔ FiniteDimensional K s :=
+theorem fg_iff_finiteDimensional (s : Submodule K V) : s.FG ↔ FiniteDimensional K s :=
   ⟨fun h => Module.finite_def.2 <| (fg_top s).2 h, fun h => (fg_top s).1 <| Module.finite_def.1 h⟩
 #align submodule.fg_iff_finite_dimensional Submodule.fg_iff_finiteDimensional
 
diff --git a/Mathlib/RingTheory/Adjoin/Fg.lean b/Mathlib/RingTheory/Adjoin/FG.lean
similarity index 87%
rename from Mathlib/RingTheory/Adjoin/Fg.lean
rename to Mathlib/RingTheory/Adjoin/FG.lean
index 231ce17de5fde..bdf84ed49bc82 100644
--- a/Mathlib/RingTheory/Adjoin/Fg.lean
+++ b/Mathlib/RingTheory/Adjoin/FG.lean
@@ -19,7 +19,7 @@ This file develops the basic theory of finitely-generated subalgebras.
 
 ## Definitions
 
-* `Fg (S : Subalgebra R A)` : A predicate saying that the subalgebra is finitely-generated
+* `FG (S : Subalgebra R A)` : A predicate saying that the subalgebra is finitely-generated
 as an A-algebra
 
 ## Tags
@@ -40,8 +40,8 @@ namespace Algebra
 variable {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A]
   {s t : Set A}
 
-theorem fg_trans (h1 : (adjoin R s).toSubmodule.Fg) (h2 : (adjoin (adjoin R s) t).toSubmodule.Fg) :
-    (adjoin R (s ∪ t)).toSubmodule.Fg := by
+theorem fg_trans (h1 : (adjoin R s).toSubmodule.FG) (h2 : (adjoin (adjoin R s) t).toSubmodule.FG) :
+    (adjoin R (s ∪ t)).toSubmodule.FG := by
   rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
   rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
   refine' fg_def.2 ⟨p * q, hp.mul hq, le_antisymm _ _⟩
@@ -93,23 +93,23 @@ variable [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
 
 /-- A subalgebra `S` is finitely generated if there exists `t : finset A` such that
 `algebra.adjoin R t = S`. -/
-def Fg (S : Subalgebra R A) : Prop :=
+def FG (S : Subalgebra R A) : Prop :=
   ∃ t : Finset A, Algebra.adjoin R ↑t = S
-#align subalgebra.fg Subalgebra.Fg
+#align subalgebra.fg Subalgebra.FG
 
-theorem fg_adjoin_finset (s : Finset A) : (Algebra.adjoin R (↑s : Set A)).Fg :=
+theorem fg_adjoin_finset (s : Finset A) : (Algebra.adjoin R (↑s : Set A)).FG :=
   ⟨s, rfl⟩
 #align subalgebra.fg_adjoin_finset Subalgebra.fg_adjoin_finset
 
-theorem fg_def {S : Subalgebra R A} : S.Fg ↔ ∃ t : Set A, Set.Finite t ∧ Algebra.adjoin R t = S :=
+theorem fg_def {S : Subalgebra R A} : S.FG ↔ ∃ t : Set A, Set.Finite t ∧ Algebra.adjoin R t = S :=
   Iff.symm Set.exists_finite_iff_finset
 #align subalgebra.fg_def Subalgebra.fg_def
 
-theorem fg_bot : (⊥ : Subalgebra R A).Fg :=
+theorem fg_bot : (⊥ : Subalgebra R A).FG :=
   ⟨∅, Finset.coe_empty ▸ Algebra.adjoin_empty R A⟩
 #align subalgebra.fg_bot Subalgebra.fg_bot
 
-theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.Fg → S.Fg :=
+theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.FG → S.FG :=
   fun ⟨t, ht⟩ ↦ ⟨t, le_antisymm
     (Algebra.adjoin_le fun x hx ↦ show x ∈ Subalgebra.toSubmodule S from ht ▸ subset_span hx) <|
     show Subalgebra.toSubmodule S ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑t) from fun x hx ↦
@@ -119,19 +119,19 @@ theorem fg_of_fg_toSubmodule {S : Subalgebra R A} : S.toSubmodule.Fg → S.Fg :=
           exact hx)⟩
 #align subalgebra.fg_of_fg_to_submodule Subalgebra.fg_of_fg_toSubmodule
 
-theorem fg_of_noetherian [IsNoetherian R A] (S : Subalgebra R A) : S.Fg :=
+theorem fg_of_noetherian [IsNoetherian R A] (S : Subalgebra R A) : S.FG :=
   fg_of_fg_toSubmodule (IsNoetherian.noetherian (Subalgebra.toSubmodule S))
 #align subalgebra.fg_of_noetherian Subalgebra.fg_of_noetherian
 
-theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).Fg) : (⊤ : Subalgebra R A).Fg :=
+theorem fg_of_submodule_fg (h : (⊤ : Submodule R A).FG) : (⊤ : Subalgebra R A).FG :=
   let ⟨s, hs⟩ := h
   ⟨s, toSubmodule.injective <| by
     rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
     exact Algebra.subset_adjoin⟩
 #align subalgebra.fg_of_submodule_fg Subalgebra.fg_of_submodule_fg
 
-theorem Fg.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.Fg) (hT : T.Fg) :
-    (S.prod T).Fg := by
+theorem FG.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.FG) (hT : T.FG) :
+    (S.prod T).FG := by
   obtain ⟨s, hs⟩ := fg_def.1 hS
   obtain ⟨t, ht⟩ := fg_def.1 hT
   rw [← hs.2, ← ht.2]
@@ -139,21 +139,21 @@ theorem Fg.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.Fg) (hT : T.Fg
     Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
       (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
     Algebra.adjoin_inl_union_inr_eq_prod R s t⟩
-#align subalgebra.fg.prod Subalgebra.Fg.prod
+#align subalgebra.fg.prod Subalgebra.FG.prod
 
 section
 
 open Classical
 
-theorem Fg.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.Fg) : (S.map f).Fg :=
+theorem FG.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG :=
   let ⟨s, hs⟩ := hs
   ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
-#align subalgebra.fg.map Subalgebra.Fg.map
+#align subalgebra.fg.map Subalgebra.FG.map
 
 end
 
 theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f)
-    (hs : (S.map f).Fg) : S.Fg :=
+    (hs : (S.map f).FG) : S.FG :=
   let ⟨s, hs⟩ := hs
   ⟨s.preimage f fun _ _ _ _ h ↦ hf h,
     map_injective hf <| by
@@ -162,10 +162,10 @@ theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Inj
       exact map_mono le_top⟩
 #align subalgebra.fg_of_fg_map Subalgebra.fg_of_fg_map
 
-theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).Fg ↔ S.Fg :=
+theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).FG ↔ S.FG :=
   ⟨fun h ↦ by
     rw [← S.range_val, ← Algebra.map_top]
-    exact Fg.map _ h, fun h ↦
+    exact FG.map _ h, fun h ↦
     fg_of_fg_map _ S.val Subtype.val_injective <| by
       rw [Algebra.map_top, range_val]
       exact h⟩
@@ -205,7 +205,7 @@ variable {R : Type u} {A : Type v} {B : Type w}
 
 variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 
-theorem isNoetherianRing_of_fg {S : Subalgebra R A} (HS : S.Fg) [IsNoetherianRing R] :
+theorem isNoetherianRing_of_fg {S : Subalgebra R A} (HS : S.FG) [IsNoetherianRing R] :
     IsNoetherianRing S :=
   let ⟨t, ht⟩ := HS
   ht ▸ (Algebra.adjoin_eq_range R (↑t : Set A)).symm ▸ AlgHom.isNoetherianRing_range _
diff --git a/Mathlib/RingTheory/Adjoin/Tower.lean b/Mathlib/RingTheory/Adjoin/Tower.lean
index 7cbc25aa805a2..dac952470ad50 100644
--- a/Mathlib/RingTheory/Adjoin/Tower.lean
+++ b/Mathlib/RingTheory/Adjoin/Tower.lean
@@ -8,7 +8,7 @@ Authors: Kenny Lau
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.RingTheory.Adjoin.Fg
+import Mathlib.RingTheory.Adjoin.FG
 
 /-!
 # Adjoining elements and being finitely generated in an algebra tower
@@ -75,8 +75,8 @@ section
 open Classical
 
 theorem Algebra.fg_trans' {R S A : Type _} [CommSemiring R] [CommSemiring S] [CommSemiring A]
-    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).Fg)
-    (hSA : (⊤ : Subalgebra S A).Fg) : (⊤ : Subalgebra R A).Fg :=
+    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG)
+    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG :=
   let ⟨s, hs⟩ := hRS
   let ⟨t, ht⟩ := hSA
   ⟨s.image (algebraMap S A) ∪ t, by
@@ -101,8 +101,8 @@ open Finset Submodule
 
 open Classical
 
-theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).Fg) (hBC : (⊤ : Submodule B C).Fg) :
-    ∃ B₀ : Subalgebra A B, B₀.Fg ∧ (⊤ : Submodule B₀ C).Fg := by
+theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) :
+    ∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG := by
   cases' hAC with x hx
   cases' hBC with y hy
   have := hy
@@ -162,9 +162,9 @@ A is noetherian, and C is algebra-finite over A, and C is module-finite over B,
 then B is algebra-finite over A.
 
 References: Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17. -/
-theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).Fg)
-    (hBC : (⊤ : Submodule B C).Fg) (hBCi : Function.Injective (algebraMap B C)) :
-    (⊤ : Subalgebra A B).Fg :=
+theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG)
+    (hBC : (⊤ : Submodule B C).FG) (hBCi : Function.Injective (algebraMap B C)) :
+    (⊤ : Subalgebra A B).FG :=
   let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC
   Algebra.fg_trans' (B₀.fg_top.2 hAB₀) <|
     Subalgebra.fg_of_submodule_fg <|
@@ -176,4 +176,3 @@ theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).Fg)
 end Ring
 
 end ArtinTate
-
diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean
index 395e52e4bdc72..050444dab1fc2 100644
--- a/Mathlib/RingTheory/FiniteType.lean
+++ b/Mathlib/RingTheory/FiniteType.lean
@@ -37,7 +37,7 @@ variable (R) (A : Type u) (B M N : Type _)
 /-- An algebra over a commutative semiring is of `FiniteType` if it is finitely generated
 over the base ring as algebra. -/
 class Algebra.FiniteType [CommSemiring R] [Semiring A] [Algebra R A] : Prop where
-  out : (⊤ : Subalgebra R A).Fg
+  out : (⊤ : Subalgebra R A).FG
 #align algebra.finite_type Algebra.FiniteType
 
 namespace Module
@@ -180,7 +180,7 @@ theorem isNoetherianRing (R S : Type _) [CommRing R] [CommRing S] [Algebra R S]
 #align algebra.finite_type.is_noetherian_ring Algebra.FiniteType.isNoetherianRing
 
 theorem _root_.Subalgebra.fg_iff_finiteType {R A : Type _} [CommSemiring R]
-    [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.Fg ↔ Algebra.FiniteType R S :=
+    [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.FG ↔ Algebra.FiniteType R S :=
   S.fg_top.symm.trans ⟨fun h => ⟨h⟩, fun h => h.out⟩
 #align subalgebra.fg_iff_finite_type Subalgebra.fg_iff_finiteType
 
@@ -449,7 +449,7 @@ variable (R M)
 
 /-- If an additive monoid `M` is finitely generated then `AddMonoidAlgebra R M` is of finite
 type. -/
-instance finiteType_of_fg [CommRing R] [h : AddMonoid.Fg M] :
+instance finiteType_of_fg [CommRing R] [h : AddMonoid.FG M] :
     FiniteType R (AddMonoidAlgebra R M) := by
   obtain ⟨S, hS⟩ := h.out
   exact (FiniteType.mvPolynomial R (S : Set M)).of_surjective
@@ -462,7 +462,7 @@ variable {R M}
 /-- An additive monoid `M` is finitely generated if and only if `AddMonoidAlgebra R M` is of
 finite type. -/
 theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
-    FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.Fg M := by
+    FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M := by
   refine' ⟨fun h => _, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
   obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
   refine' AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => _⟩
@@ -474,14 +474,14 @@ theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
 
 /-- If `AddMonoidAlgebra R M` is of finite type then `M` is finitely generated. -/
 theorem fg_of_finiteType [CommRing R] [Nontrivial R] [h : FiniteType R (AddMonoidAlgebra R M)] :
-    AddMonoid.Fg M :=
+    AddMonoid.FG M :=
   finiteType_iff_fg.1 h
 #align add_monoid_algebra.fg_of_finite_type AddMonoidAlgebra.fg_of_finiteType
 
 /-- An additive group `G` is finitely generated if and only if `AddMonoidAlgebra R G` is of
 finite type. -/
 theorem finiteType_iff_group_fg {G : Type _} [AddCommGroup G] [CommRing R] [Nontrivial R] :
-    FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.Fg G := by
+    FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G := by
   simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg
 #align add_monoid_algebra.finite_type_iff_group_fg AddMonoidAlgebra.finiteType_iff_group_fg
 
@@ -601,13 +601,13 @@ theorem mvPolynomial_aeval_of_surjective_of_closure [CommSemiring R] {S : Set M}
 #align monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure
 
 /-- If a monoid `M` is finitely generated then `MonoidAlgebra R M` is of finite type. -/
-instance finiteType_of_fg [CommRing R] [Monoid.Fg M] : FiniteType R (MonoidAlgebra R M) :=
+instance finiteType_of_fg [CommRing R] [Monoid.FG M] : FiniteType R (MonoidAlgebra R M) :=
   (AddMonoidAlgebra.finiteType_of_fg R (Additive M)).equiv (toAdditiveAlgEquiv R M).symm
 #align monoid_algebra.finite_type_of_fg MonoidAlgebra.finiteType_of_fg
 
 /-- A monoid `M` is finitely generated if and only if `MonoidAlgebra R M` is of finite type. -/
 theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
-    FiniteType R (MonoidAlgebra R M) ↔ Monoid.Fg M :=
+    FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M :=
   ⟨fun h =>
     Monoid.fg_iff_add_fg.2 <|
       AddMonoidAlgebra.finiteType_iff_fg.1 <| h.equiv <| toAdditiveAlgEquiv R M,
@@ -616,13 +616,13 @@ theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
 
 /-- If `MonoidAlgebra R M` is of finite type then `M` is finitely generated. -/
 theorem fg_of_finiteType [CommRing R] [Nontrivial R] [h : FiniteType R (MonoidAlgebra R M)] :
-    Monoid.Fg M :=
+    Monoid.FG M :=
   finiteType_iff_fg.1 h
 #align monoid_algebra.fg_of_finite_type MonoidAlgebra.fg_of_finiteType
 
 /-- A group `G` is finitely generated if and only if `AddMonoidAlgebra R G` is of finite type. -/
 theorem finiteType_iff_group_fg {G : Type _} [CommGroup G] [CommRing R] [Nontrivial R] :
-    FiniteType R (MonoidAlgebra R G) ↔ Group.Fg G := by
+    FiniteType R (MonoidAlgebra R G) ↔ Group.FG G := by
   simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg
 #align monoid_algebra.finite_type_iff_group_fg MonoidAlgebra.finiteType_iff_group_fg
 
diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
index 509892618a0f3..0c5309e9cf7d0 100644
--- a/Mathlib/RingTheory/Finiteness.lean
+++ b/Mathlib/RingTheory/Finiteness.lean
@@ -20,7 +20,7 @@ In this file we define a notion of finiteness that is common in commutative alge
 
 ## Main declarations
 
-- `Submodule.Fg`, `Ideal.Fg`
+- `Submodule.FG`, `Ideal.FG`
   These express that some object is finitely generated as *submodule* over some base ring.
 
 - `Module.Finite`, `RingHom.Finite`, `AlgHom.Finite`
@@ -46,30 +46,30 @@ variable {R : Type _} {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
 open Set
 
 /-- A submodule of `M` is finitely generated if it is the span of a finite subset of `M`. -/
-def Fg (N : Submodule R M) : Prop :=
+def FG (N : Submodule R M) : Prop :=
   ∃ S : Finset M, Submodule.span R ↑S = N
-#align submodule.fg Submodule.Fg
+#align submodule.fg Submodule.FG
 
-theorem fg_def {N : Submodule R M} : N.Fg ↔ ∃ S : Set M, S.Finite ∧ span R S = N :=
+theorem fg_def {N : Submodule R M} : N.FG ↔ ∃ S : Set M, S.Finite ∧ span R S = N :=
   ⟨fun ⟨t, h⟩ => ⟨_, Finset.finite_toSet t, h⟩, by
     rintro ⟨t', h, rfl⟩
     rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
     exact ⟨t, rfl⟩⟩
 #align submodule.fg_def Submodule.fg_def
 
-theorem fg_iff_addSubmonoid_fg (P : Submodule ℕ M) : P.Fg ↔ P.toAddSubmonoid.Fg :=
+theorem fg_iff_addSubmonoid_fg (P : Submodule ℕ M) : P.FG ↔ P.toAddSubmonoid.FG :=
   ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_nat_eq_addSubmonoid_closure] using hS⟩, fun ⟨S, hS⟩ =>
     ⟨S, by simpa [← span_nat_eq_addSubmonoid_closure] using hS⟩⟩
 #align submodule.fg_iff_add_submonoid_fg Submodule.fg_iff_addSubmonoid_fg
 
 theorem fg_iff_add_subgroup_fg {G : Type _} [AddCommGroup G] (P : Submodule ℤ G) :
-    P.Fg ↔ P.toAddSubgroup.Fg :=
+    P.FG ↔ P.toAddSubgroup.FG :=
   ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_int_eq_addSubgroup_closure] using hS⟩, fun ⟨S, hS⟩ =>
     ⟨S, by simpa [← span_int_eq_addSubgroup_closure] using hS⟩⟩
 #align submodule.fg_iff_add_subgroup_fg Submodule.fg_iff_add_subgroup_fg
 
 theorem fg_iff_exists_fin_generating_family {N : Submodule R M} :
-    N.Fg ↔ ∃ (n : ℕ)(s : Fin n → M), span R (range s) = N := by
+    N.FG ↔ ∃ (n : ℕ)(s : Fin n → M), span R (range s) = N := by
   rw [fg_def]
   constructor
   · rintro ⟨S, Sfin, hS⟩
@@ -82,7 +82,7 @@ theorem fg_iff_exists_fin_generating_family {N : Submodule R M} :
 /-- **Nakayama's Lemma**. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2,
 [Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV) -/
 theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type _} [CommRing R] {M : Type _}
-    [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.Fg) (hin : N ≤ I • N) :
+    [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) :
     ∃ r : R, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = (0 : M) := by
   rw [fg_def] at hn
   rcases hn with ⟨s, hfs, hs⟩
@@ -137,23 +137,23 @@ theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type _} [CommR
 #align submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
 
 theorem exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type _} [CommRing R] {M : Type _}
-    [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.Fg) (hin : N ≤ I • N) :
+    [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) :
     ∃ r ∈ I, ∀ n ∈ N, r • n = n := by
   obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin
   exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩
 #align submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul
 
-theorem fg_bot : (⊥ : Submodule R M).Fg :=
+theorem fg_bot : (⊥ : Submodule R M).FG :=
   ⟨∅, by rw [Finset.coe_empty, span_empty]⟩
 #align submodule.fg_bot Submodule.fg_bot
 
 theorem _root_.Subalgebra.fg_bot_toSubmodule {R A : Type _} [CommSemiring R] [Semiring A]
-    [Algebra R A] : (⊥ : Subalgebra R A).toSubmodule.Fg :=
+    [Algebra R A] : (⊥ : Subalgebra R A).toSubmodule.FG :=
   ⟨{1}, by simp [Algebra.toSubmodule_bot]⟩
 #align subalgebra.fg_bot_to_submodule Subalgebra.fg_bot_toSubmodule
 
 theorem fg_unit {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) :
-    (I : Submodule R A).Fg := by
+    (I : Submodule R A).FG := by
   have : (1 : A) ∈ (I * ↑I⁻¹ : Submodule R A) := by
     rw [I.mul_inv]
     exact one_le.mp le_rfl
@@ -167,35 +167,35 @@ theorem fg_unit {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A] (I :
 #align submodule.fg_unit Submodule.fg_unit
 
 theorem fg_of_isUnit {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A}
-    (hI : IsUnit I) : I.Fg :=
+    (hI : IsUnit I) : I.FG :=
   fg_unit hI.unit
 #align submodule.fg_of_is_unit Submodule.fg_of_isUnit
 
-theorem fg_span {s : Set M} (hs : s.Finite) : Fg (span R s) :=
+theorem fg_span {s : Set M} (hs : s.Finite) : FG (span R s) :=
   ⟨hs.toFinset, by rw [hs.coe_toFinset]⟩
 #align submodule.fg_span Submodule.fg_span
 
-theorem fg_span_singleton (x : M) : Fg (R ∙ x) :=
+theorem fg_span_singleton (x : M) : FG (R ∙ x) :=
   fg_span (finite_singleton x)
 #align submodule.fg_span_singleton Submodule.fg_span_singleton
 
-theorem Fg.sup {N₁ N₂ : Submodule R M} (hN₁ : N₁.Fg) (hN₂ : N₂.Fg) : (N₁ ⊔ N₂).Fg :=
+theorem FG.sup {N₁ N₂ : Submodule R M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG :=
   let ⟨t₁, ht₁⟩ := fg_def.1 hN₁
   let ⟨t₂, ht₂⟩ := fg_def.1 hN₂
   fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
-#align submodule.fg.sup Submodule.Fg.sup
+#align submodule.fg.sup Submodule.FG.sup
 
-theorem fg_finset_sup {ι : Type _} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).Fg) :
-    (s.sup N).Fg :=
+theorem fg_finset_sup {ι : Type _} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) :
+    (s.sup N).FG :=
   Finset.sup_induction fg_bot (fun _ ha _ hb => ha.sup hb) h
 #align submodule.fg_finset_sup Submodule.fg_finset_sup
 
-theorem fg_biSup {ι : Type _} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).Fg) :
-    (⨆ i ∈ s, N i).Fg := by simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h
+theorem fg_biSup {ι : Type _} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) :
+    (⨆ i ∈ s, N i).FG := by simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h
 #align submodule.fg_bsupr Submodule.fg_biSup
 
-theorem fg_iSup {ι : Type _} [Finite ι] (N : ι → Submodule R M) (h : ∀ i, (N i).Fg) :
-    (iSup N).Fg := by
+theorem fg_iSup {ι : Type _} [Finite ι] (N : ι → Submodule R M) (h : ∀ i, (N i).FG) :
+    (iSup N).FG := by
   cases nonempty_fintype ι
   simpa using fg_biSup Finset.univ N fun i _ => h i
 #align submodule.fg_supr Submodule.fg_iSup
@@ -204,15 +204,15 @@ variable {P : Type _} [AddCommMonoid P] [Module R P]
 
 variable (f : M →ₗ[R] P)
 
-theorem Fg.map {N : Submodule R M} (hs : N.Fg) : (N.map f).Fg :=
+theorem FG.map {N : Submodule R M} (hs : N.FG) : (N.map f).FG :=
   let ⟨t, ht⟩ := fg_def.1 hs
   fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩
-#align submodule.fg.map Submodule.Fg.map
+#align submodule.fg.map Submodule.FG.map
 
 variable {f}
 
 theorem fg_of_fg_map_injective (f : M →ₗ[R] P) (hf : Function.Injective f) {N : Submodule R M}
-    (hfn : (N.map f).Fg) : N.Fg :=
+    (hfn : (N.map f).FG) : N.FG :=
   let ⟨t, ht⟩ := hfn
   ⟨t.preimage f fun x _ y _ h => hf h,
     Submodule.map_injective_of_injective hf <| by
@@ -229,31 +229,31 @@ alias LinearMap.instSemilinearMapClassLinearMap ← instSLMC
 theorem fg_of_fg_map {R M P : Type _} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P]
     [Module R P] (f : M →ₗ[R] P)
     (hf : @LinearMap.ker R R M P _ _ _ _ _ _ (RingHom.id _) _ instSLMC f = ⊥) {N : Submodule R M}
-    (hfn : (@map R R M P _ _ _ _ _ _ (RingHom.id _) _ _ instSLMC f N).Fg) : N.Fg :=
+    (hfn : (@map R R M P _ _ _ _ _ _ (RingHom.id _) _ _ instSLMC f N).FG) : N.FG :=
   fg_of_fg_map_injective f (LinearMap.ker_eq_bot.1 hf) hfn
 #align submodule.fg_of_fg_map Submodule.fg_of_fg_map
 
-theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).Fg ↔ N.Fg :=
+theorem fg_top (N : Submodule R M) : (⊤ : Submodule R N).FG ↔ N.FG :=
   ⟨fun h => N.range_subtype ▸ map_top N.subtype ▸ h.map _, fun h =>
     fg_of_fg_map_injective N.subtype Subtype.val_injective <| by rwa [map_top, range_subtype]⟩
 #align submodule.fg_top Submodule.fg_top
 
-theorem fg_of_linearEquiv (e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).Fg) : (⊤ : Submodule R M).Fg :=
+theorem fg_of_linearEquiv (e : M ≃ₗ[R] P) (h : (⊤ : Submodule R P).FG) : (⊤ : Submodule R M).FG :=
   e.symm.range ▸ map_top (e.symm : P →ₗ[R] M) ▸ h.map _
 #align submodule.fg_of_linear_equiv Submodule.fg_of_linearEquiv
 
-theorem Fg.prod {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.Fg) (hsc : sc.Fg) :
-    (sb.prod sc).Fg :=
+theorem FG.prod {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.FG) (hsc : sc.FG) :
+    (sb.prod sc).FG :=
   let ⟨tb, htb⟩ := fg_def.1 hsb
   let ⟨tc, htc⟩ := fg_def.1 hsc
   fg_def.2
     ⟨LinearMap.inl R M P '' tb ∪ LinearMap.inr R M P '' tc, (htb.1.image _).union (htc.1.image _),
       by rw [LinearMap.span_inl_union_inr, htb.2, htc.2]⟩
-#align submodule.fg.prod Submodule.Fg.prod
+#align submodule.fg.prod Submodule.FG.prod
 
 theorem fg_pi {ι : Type _} {M : ι → Type _} [Finite ι] [∀ i, AddCommMonoid (M i)]
-    [∀ i, Module R (M i)] {p : ∀ i, Submodule R (M i)} (hsb : ∀ i, (p i).Fg) :
-    (Submodule.pi Set.univ p).Fg := by
+    [∀ i, Module R (M i)] {p : ∀ i, Submodule R (M i)} (hsb : ∀ i, (p i).FG) :
+    (Submodule.pi Set.univ p).FG := by
   classical
     simp_rw [fg_def] at hsb⊢
     choose t htf hts using hsb
@@ -277,8 +277,8 @@ theorem fg_of_fg_map_of_fg_inf_ker {R M P : Type _} [Ring R] [AddCommGroup M] [M
     [AddCommGroup P] [Module R P] (f : M →ₗ[R] P) {s : Submodule R M}
     -- Porting note: Lean having trouble both unifying for SLMC and then synthesizing once unified
     -- With etaExperiment, we don't need the @s in the following statement.
-    (hs1 : (@map R R M P _ _ _ _ _ _ (RingHom.id _) _ _ instSLMC f s).Fg)
-    (hs2 : (s ⊓ @LinearMap.ker R R M P _ _ _ _ _ _ (RingHom.id _) _ instSLMC f).Fg) : s.Fg := by
+    (hs1 : (@map R R M P _ _ _ _ _ _ (RingHom.id _) _ _ instSLMC f s).FG)
+    (hs2 : (s ⊓ @LinearMap.ker R R M P _ _ _ _ _ _ (RingHom.id _) _ instSLMC f).FG) : s.FG := by
   haveI := Classical.decEq R
   haveI := Classical.decEq M
   haveI := Classical.decEq P
@@ -357,7 +357,7 @@ theorem fg_of_fg_map_of_fg_inf_ker {R M P : Type _} [Ring R] [AddCommGroup M] [M
 
 theorem fg_induction (R M : Type _) [Semiring R] [AddCommMonoid M] [Module R M]
     (P : Submodule R M → Prop) (h₁ : ∀ x, P (Submodule.span R {x}))
-    (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.Fg) : P N := by
+    (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.FG) : P N := by
   classical
     obtain ⟨s, rfl⟩ := hN
     induction s using Finset.induction
@@ -373,11 +373,11 @@ theorem fg_ker_comp {R M N P : Type _} [Ring R] [AddCommGroup M] [Module R M] [A
     [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
     -- Porting note: more help both unifying and finding instSLMC
     -- With etaExperiment, we don't need the @s in the following statement.
-    (hf1 : (@LinearMap.ker R R M N _ _ _ _ _ _ (RingHom.id _) _ instSLMC f).Fg)
-    (hf2 : (@LinearMap.ker R R N P _ _ _ _ _ _ (RingHom.id _) _ instSLMC g).Fg)
+    (hf1 : (@LinearMap.ker R R M N _ _ _ _ _ _ (RingHom.id _) _ instSLMC f).FG)
+    (hf2 : (@LinearMap.ker R R N P _ _ _ _ _ _ (RingHom.id _) _ instSLMC g).FG)
     (hsur : Function.Surjective <| asFun f) :
     (@LinearMap.comp R R R M N P _ _ _ _ _ _ _ _ _
-      (RingHom.id _) (RingHom.id _) (RingHom.id _) _ g f).ker.Fg := by
+      (RingHom.id _) (RingHom.id _) (RingHom.id _) _ g f).ker.FG := by
   rw [LinearMap.ker_comp]
   apply fg_of_fg_map_of_fg_inf_ker f
   · rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]
@@ -389,14 +389,14 @@ theorem fg_ker_comp {R M N P : Type _} [Ring R] [AddCommGroup M] [Module R M] [A
 
 theorem fg_restrictScalars {R S M : Type _} [CommSemiring R] [Semiring S] [Algebra R S]
     [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M] (N : Submodule S M)
-    (hfin : N.Fg) (h : Function.Surjective (algebraMap R S)) :
-    (Submodule.restrictScalars R N).Fg := by
+    (hfin : N.FG) (h : Function.Surjective (algebraMap R S)) :
+    (Submodule.restrictScalars R N).FG := by
   obtain ⟨X, rfl⟩ := hfin
   use X
   exact (Submodule.restrictScalars_span R S h (X : Set M)).symm
 #align submodule.fg_restrict_scalars Submodule.fg_restrictScalars
 
-theorem Fg.stablizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.Fg) (N : ℕ →o Submodule R M)
+theorem FG.stablizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.FG) (N : ℕ →o Submodule R M)
     (H : iSup N = M') : ∃ n, M' = N n := by
   obtain ⟨S, hS⟩ := hM'
   have : ∀ s : S, ∃ n, (s : M) ∈ N n := fun s =>
@@ -413,10 +413,10 @@ theorem Fg.stablizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.Fg) (N : ℕ →o
     exact N.2 (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)
   · rw [← H]
     exact le_iSup _ _
-#align submodule.fg.stablizes_of_supr_eq Submodule.Fg.stablizes_of_iSup_eq
+#align submodule.fg.stablizes_of_supr_eq Submodule.FG.stablizes_of_iSup_eq
 
 /-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
-theorem fg_iff_compact (s : Submodule R M) : s.Fg ↔ CompleteLattice.IsCompactElement s := by
+theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactElement s := by
   classical
     -- Introduce shorthand for span of an element
     let sp : M → Submodule R M := fun a => span R {a}
@@ -458,14 +458,14 @@ variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
 
 variable [Module R M] [Module R N] [Module R P]
 
-theorem Fg.map₂ (f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N} (hp : p.Fg)
-    (hq : q.Fg) : (map₂ f p q).Fg :=
+theorem FG.map₂ (f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N} (hp : p.FG)
+    (hq : q.FG) : (map₂ f p q).FG :=
   let ⟨sm, hfm, hm⟩ := fg_def.1 hp
   let ⟨sn, hfn, hn⟩ := fg_def.1 hq
   fg_def.2
     ⟨Set.image2 (fun m n => f m n) sm sn, hfm.image2 _ hfn,
       map₂_span_span R f sm sn ▸ hm ▸ hn ▸ rfl⟩
-#align submodule.fg.map₂ Submodule.Fg.map₂
+#align submodule.fg.map₂ Submodule.FG.map₂
 
 end Map₂
 
@@ -475,13 +475,13 @@ variable {R : Type _} {A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
 
 variable {M N : Submodule R A}
 
-theorem Fg.mul (hm : M.Fg) (hn : N.Fg) : (M * N).Fg :=
+theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG :=
   hm.map₂ _ hn
-#align submodule.fg.mul Submodule.Fg.mul
+#align submodule.fg.mul Submodule.FG.mul
 
-theorem Fg.pow (h : M.Fg) (n : ℕ) : (M ^ n).Fg :=
+theorem FG.pow (h : M.FG) (n : ℕ) : (M ^ n).FG :=
   Nat.recOn n ⟨{1}, by simp [one_eq_span]⟩ fun n ih => by simpa [pow_succ] using h.mul ih
-#align submodule.fg.pow Submodule.Fg.pow
+#align submodule.fg.pow Submodule.FG.pow
 
 end Mul
 
@@ -493,26 +493,26 @@ variable {R : Type _} {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
 
 /-- An ideal of `R` is finitely generated if it is the span of a finite subset of `R`.
 
-This is defeq to `Submodule.Fg`, but unfolds more nicely. -/
-def Fg (I : Ideal R) : Prop :=
+This is defeq to `Submodule.FG`, but unfolds more nicely. -/
+def FG (I : Ideal R) : Prop :=
   ∃ S : Finset R, Ideal.span ↑S = I
-#align ideal.fg Ideal.Fg
+#align ideal.fg Ideal.FG
 
 /-- The image of a finitely generated ideal is finitely generated.
 
-This is the `ideal` version of `Submodule.Fg.map`. -/
-theorem Fg.map {R S : Type _} [Semiring R] [Semiring S] {I : Ideal R} (h : I.Fg) (f : R →+* S) :
-    (I.map f).Fg := by
+This is the `ideal` version of `Submodule.FG.map`. -/
+theorem FG.map {R S : Type _} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) :
+    (I.map f).FG := by
   classical
     obtain ⟨s, hs⟩ := h
     refine' ⟨s.image f, _⟩
     rw [Finset.coe_image, ← Ideal.map_span, hs]
-#align ideal.fg.map Ideal.Fg.map
+#align ideal.fg.map Ideal.FG.map
 
 set_option synthInstance.etaExperiment true in
 theorem fg_ker_comp {R S A : Type _} [CommRing R] [CommRing S] [CommRing A] (f : R →+* S)
-    (g : S →+* A) (hf : f.ker.Fg) (hg : g.ker.Fg) (hsur : Function.Surjective f) :
-    (g.comp f).ker.Fg := by
+    (g : S →+* A) (hf : f.ker.FG) (hg : g.ker.FG) (hsur : Function.Surjective f) :
+    (g.comp f).ker.FG := by
   letI : Algebra R S := RingHom.toAlgebra f
   letI : Algebra R A := RingHom.toAlgebra (g.comp f)
   letI : Algebra S A := RingHom.toAlgebra g
@@ -522,7 +522,7 @@ theorem fg_ker_comp {R S A : Type _} [CommRing R] [CommRing S] [CommRing A] (f :
   exact Submodule.fg_ker_comp f₁ g₁ hf (Submodule.fg_restrictScalars (RingHom.ker g) hg hsur) hsur
 #align ideal.fg_ker_comp Ideal.fg_ker_comp
 
-theorem exists_radical_pow_le_of_fg {R : Type _} [CommSemiring R] (I : Ideal R) (h : I.radical.Fg) :
+theorem exists_radical_pow_le_of_fg {R : Type _} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) :
     ∃ n : ℕ, I.radical ^ n ≤ I := by
   have := le_refl I.radical; revert this
   refine' Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) _ _ _ h
@@ -551,7 +551,7 @@ variable (R A B M N : Type _)
 
 /-- A module over a semiring is `Finite` if it is finitely generated as a module. -/
 class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
-  out : (⊤ : Submodule R M).Fg
+  out : (⊤ : Submodule R M).FG
 #align module.finite Module.Finite
 
 attribute [inherit_doc Module.Finite] Module.Finite.out
@@ -561,7 +561,7 @@ namespace Module
 variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
 
 theorem finite_def {R M} [Semiring R] [AddCommMonoid M] [Module R M] :
-    Finite R M ↔ (⊤ : Submodule R M).Fg :=
+    Finite R M ↔ (⊤ : Submodule R M).FG :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 #align module.finite_def Module.finite_def
 
@@ -569,12 +569,12 @@ namespace Finite
 
 open Submodule Set
 
-theorem iff_addMonoid_fg {M : Type _} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.Fg M :=
+theorem iff_addMonoid_fg {M : Type _} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M :=
   ⟨fun h => AddMonoid.fg_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).1 (finite_def.1 h), fun h =>
     finite_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).2 (AddMonoid.fg_def.1 h)⟩
 #align module.finite.iff_add_monoid_fg Module.Finite.iff_addMonoid_fg
 
-theorem iff_addGroup_fg {G : Type _} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.Fg G :=
+theorem iff_addGroup_fg {G : Type _} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G :=
   ⟨fun h => AddGroup.fg_def.2 <| (Submodule.fg_iff_add_subgroup_fg ⊤).1 (finite_def.1 h), fun h =>
     finite_def.2 <| (Submodule.fg_iff_add_subgroup_fg ⊤).2 (AddGroup.fg_def.1 h)⟩
 #align module.finite.iff_add_group_fg Module.Finite.iff_addGroup_fg
diff --git a/Mathlib/RingTheory/Flat.lean b/Mathlib/RingTheory/Flat.lean
index 0e385b4859af3..06cb289bc461c 100644
--- a/Mathlib/RingTheory/Flat.lean
+++ b/Mathlib/RingTheory/Flat.lean
@@ -62,7 +62,7 @@ open TensorProduct
 /-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`,
 the canonical map `I ⊗ M →ₗ M` is injective. -/
 class Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Prop where
-  out : ∀ ⦃I : Ideal R⦄ (_ : I.Fg), Injective (TensorProduct.lift ((lsmul R M).comp I.subtype))
+  out : ∀ ⦃I : Ideal R⦄ (_ : I.FG), Injective (TensorProduct.lift ((lsmul R M).comp I.subtype))
 #align module.flat Module.Flat
 
 namespace Flat
diff --git a/Mathlib/RingTheory/Ideal/IdempotentFg.lean b/Mathlib/RingTheory/Ideal/IdempotentFG.lean
similarity index 95%
rename from Mathlib/RingTheory/Ideal/IdempotentFg.lean
rename to Mathlib/RingTheory/Ideal/IdempotentFG.lean
index 345088d7e378a..58a7348922e8b 100644
--- a/Mathlib/RingTheory/Ideal/IdempotentFg.lean
+++ b/Mathlib/RingTheory/Ideal/IdempotentFG.lean
@@ -20,7 +20,7 @@ namespace Ideal
 
 set_option synthInstance.etaExperiment true in
 /-- A finitely generated idempotent ideal is generated by an idempotent element -/
-theorem isIdempotentElem_iff_of_fg {R : Type _} [CommRing R] (I : Ideal R) (h : I.Fg) :
+theorem isIdempotentElem_iff_of_fg {R : Type _} [CommRing R] (I : Ideal R) (h : I.FG) :
     IsIdempotentElem I ↔ ∃ e : R, IsIdempotentElem e ∧ I = R ∙ e := by
   constructor
   · intro e
@@ -39,7 +39,7 @@ theorem isIdempotentElem_iff_of_fg {R : Type _} [CommRing R] (I : Ideal R) (h :
 #align ideal.is_idempotent_elem_iff_of_fg Ideal.isIdempotentElem_iff_of_fg
 
 theorem isIdempotentElem_iff_eq_bot_or_top {R : Type _} [CommRing R] [IsDomain R] (I : Ideal R)
-    (h : I.Fg) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ := by
+    (h : I.FG) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ := by
   constructor
   · intro H
     obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
diff --git a/Mathlib/RingTheory/Localization/InvSubmonoid.lean b/Mathlib/RingTheory/Localization/InvSubmonoid.lean
index 823806b362b3d..a3de8838d9bd8 100644
--- a/Mathlib/RingTheory/Localization/InvSubmonoid.lean
+++ b/Mathlib/RingTheory/Localization/InvSubmonoid.lean
@@ -119,7 +119,7 @@ theorem span_invSubmonoid : Submodule.span R (invSubmonoid M S : Set S) = ⊤ :=
   exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)
 #align is_localization.span_inv_submonoid IsLocalization.span_invSubmonoid
 
-theorem finiteType_of_monoid_fg [Monoid.Fg M] : Algebra.FiniteType R S := by
+theorem finiteType_of_monoid_fg [Monoid.FG M] : Algebra.FiniteType R S := by
   have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
   rw [Monoid.fg_iff_submonoid_fg] at this
   rcases this with ⟨s, hs⟩
diff --git a/Mathlib/RingTheory/Localization/Submodule.lean b/Mathlib/RingTheory/Localization/Submodule.lean
index 2afd9e51227cd..bee98bad8771b 100644
--- a/Mathlib/RingTheory/Localization/Submodule.lean
+++ b/Mathlib/RingTheory/Localization/Submodule.lean
@@ -79,8 +79,8 @@ theorem coeSubmodule_mul (I J : Ideal R) :
 
 set_option synthInstance.etaExperiment true in
 theorem coeSubmodule_fg (hS : Function.Injective (algebraMap R S)) (I : Ideal R) :
-    Submodule.Fg (coeSubmodule S I) ↔ Submodule.Fg I :=
-  ⟨Submodule.fg_of_fg_map _ (LinearMap.ker_eq_bot.mpr hS), Submodule.Fg.map _⟩
+    Submodule.FG (coeSubmodule S I) ↔ Submodule.FG I :=
+  ⟨Submodule.fg_of_fg_map _ (LinearMap.ker_eq_bot.mpr hS), Submodule.FG.map _⟩
 #align is_localization.coe_submodule_fg IsLocalization.coeSubmodule_fg
 
 set_option synthInstance.etaExperiment true in
diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean
index 4205d28693518..e62c350c5a34e 100644
--- a/Mathlib/RingTheory/Noetherian.lean
+++ b/Mathlib/RingTheory/Noetherian.lean
@@ -69,7 +69,7 @@ implemented as the predicate that all `R`-submodules of `M` are finitely generat
 -/
 -- Porting note: should this be renamed to `Noetherian`?
 class IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
-  noetherian : ∀ s : Submodule R M, s.Fg
+  noetherian : ∀ s : Submodule R M, s.FG
 #align is_noetherian IsNoetherian
 
 attribute [inherit_doc IsNoetherian] IsNoetherian.noetherian
@@ -85,12 +85,12 @@ variable [Module R M] [Module R P]
 open IsNoetherian
 
 /-- An R-module is Noetherian iff all its submodules are finitely-generated. -/
-theorem isNoetherian_def : IsNoetherian R M ↔ ∀ s : Submodule R M, s.Fg :=
+theorem isNoetherian_def : IsNoetherian R M ↔ ∀ s : Submodule R M, s.FG :=
   ⟨fun h => h.noetherian, IsNoetherian.mk⟩
 #align is_noetherian_def isNoetherian_def
 
 theorem isNoetherian_submodule {N : Submodule R M} :
-    IsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.Fg := by
+    IsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.FG := by
   refine ⟨fun ⟨hn⟩ => fun s hs =>
     have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
     Submodule.map_comap_eq_self this ▸ (hn _).map _,
@@ -103,12 +103,12 @@ theorem isNoetherian_submodule {N : Submodule R M} :
 #align is_noetherian_submodule isNoetherian_submodule
 
 theorem isNoetherian_submodule_left {N : Submodule R M} :
-    IsNoetherian R N ↔ ∀ s : Submodule R M, (N ⊓ s).Fg :=
+    IsNoetherian R N ↔ ∀ s : Submodule R M, (N ⊓ s).FG :=
   isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_left, fun H _ hs => inf_of_le_right hs ▸ H _⟩
 #align is_noetherian_submodule_left isNoetherian_submodule_left
 
 theorem isNoetherian_submodule_right {N : Submodule R M} :
-    IsNoetherian R N ↔ ∀ s : Submodule R M, (s ⊓ N).Fg :=
+    IsNoetherian R N ↔ ∀ s : Submodule R M, (s ⊓ N).FG :=
   isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_right, fun H _ hs => inf_of_le_left hs ▸ H _⟩
 #align is_noetherian_submodule_right isNoetherian_submodule_right
 
@@ -148,7 +148,7 @@ theorem isNoetherian_of_injective [IsNoetherian R P] (f : M →ₗ[R] P) (hf : F
 #align is_noetherian_of_injective isNoetherian_of_injective
 
 theorem fg_of_injective [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P)
-    (hf : Function.Injective f) : N.Fg :=
+    (hf : Function.Injective f) : N.FG :=
   haveI := isNoetherian_of_injective f hf
   IsNoetherian.noetherian N
 #align fg_of_injective fg_of_injective
@@ -193,7 +193,7 @@ theorem isNoetherian_of_ker_bot [IsNoetherian R P] (f : M →ₗ[R] P) (hf : Lin
 #align is_noetherian_of_ker_bot isNoetherian_of_ker_bot
 
 theorem fg_of_ker_bot [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P)
-    (hf : LinearMap.ker f = ⊥) : N.Fg :=
+    (hf : LinearMap.ker f = ⊥) : N.FG :=
   haveI := isNoetherian_of_ker_bot f hf
   IsNoetherian.noetherian N
 #align fg_of_ker_bot fg_of_ker_bot
@@ -311,8 +311,8 @@ theorem isNoetherian_iff_wellFounded :
 theorem isNoetherian_iff_fg_wellFounded :
     IsNoetherian R M ↔
       WellFounded
-        ((· > ·) : { N : Submodule R M // N.Fg } → { N : Submodule R M // N.Fg } → Prop) := by
-  let α := { N : Submodule R M // N.Fg }
+        ((· > ·) : { N : Submodule R M // N.FG } → { N : Submodule R M // N.FG } → Prop) := by
+  let α := { N : Submodule R M // N.FG }
   constructor
   · intro H
     let f : α ↪o Submodule R M := OrderEmbedding.subtype _
@@ -328,7 +328,7 @@ theorem isNoetherian_iff_fg_wellFounded :
     obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
     apply hx₂
     rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
-      ⟨_, Submodule.Fg.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
+      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
       sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]
     exact (le_sup_left : (R ∙ x) ≤ _) (Submodule.mem_span_singleton_self _)
 #align is_noetherian_iff_fg_well_founded isNoetherian_iff_fg_wellFounded
@@ -499,7 +499,7 @@ theorem isNoetherianRing_iff {R} [Semiring R] : IsNoetherianRing R ↔ IsNoether
 
 /-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/
 theorem isNoetherianRing_iff_ideal_fg (R : Type _) [Semiring R] :
-    IsNoetherianRing R ↔ ∀ I : Ideal R, I.Fg :=
+    IsNoetherianRing R ↔ ∀ I : Ideal R, I.FG :=
   isNoetherianRing_iff.trans isNoetherian_def
 #align is_noetherian_ring_iff_ideal_fg isNoetherianRing_iff_ideal_fg
 
@@ -539,7 +539,7 @@ theorem isNoetherian_of_tower (R) {S M} [Semiring R] [Semiring S] [AddCommMonoid
 
 set_option synthInstance.etaExperiment true in
 theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module R M]
-    (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.Fg) : IsNoetherian R N := by
+    (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) : IsNoetherian R N := by
   let ⟨s, hs⟩ := hN
   haveI := Classical.decEq M
   haveI := Classical.decEq R
@@ -574,7 +574,7 @@ theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module
 #align is_noetherian_of_fg_of_noetherian isNoetherian_of_fg_of_noetherian
 
 theorem isNoetherian_of_fg_of_noetherian' {R M} [Ring R] [AddCommGroup M] [Module R M]
-    [IsNoetherianRing R] (h : (⊤ : Submodule R M).Fg) : IsNoetherian R M :=
+    [IsNoetherianRing R] (h : (⊤ : Submodule R M).FG) : IsNoetherian R M :=
   have : IsNoetherian R (⊤ : Submodule R M) := isNoetherian_of_fg_of_noetherian _ h
   isNoetherian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl)
 #align is_noetherian_of_fg_of_noetherian' isNoetherian_of_fg_of_noetherian'
diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean
index 24f4ad9c1b4af..3c8c3f024519e 100644
--- a/Mathlib/RingTheory/Polynomial/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Basic.lean
@@ -739,7 +739,7 @@ set_option linter.uppercaseLean3 false in
 #align ideal.is_prime_map_C_of_is_prime Ideal.isPrime_map_C_of_isPrime
 
 theorem is_fg_degreeLE [IsNoetherianRing R] (I : Ideal R[X]) (n : ℕ) :
-    Submodule.Fg (I.degreeLE n) :=
+    Submodule.FG (I.degreeLE n) :=
   isNoetherian_submodule_left.1
     -- porting note: times out without explicit `R`.
     (isNoetherian_of_fg_of_noetherian _ ⟨_, (degreeLE_eq_span_X_pow (R := R)).symm⟩) _
diff --git a/Mathlib/RingTheory/ReesAlgebra.lean b/Mathlib/RingTheory/ReesAlgebra.lean
index 4ed3e29f44d5e..72762c9b9b549 100644
--- a/Mathlib/RingTheory/ReesAlgebra.lean
+++ b/Mathlib/RingTheory/ReesAlgebra.lean
@@ -116,7 +116,7 @@ theorem adjoin_monomial_eq_reesAlgebra :
 variable {I}
 
 set_option synthInstance.etaExperiment true in
-theorem reesAlgebra.fg (hI : I.Fg) : (reesAlgebra I).Fg := by
+theorem reesAlgebra.fg (hI : I.FG) : (reesAlgebra I).FG := by
   classical
     obtain ⟨s, hs⟩ := hI
     rw [← adjoin_monomial_eq_reesAlgebra, ← hs]