leanprover-community · kim-em · Apr 11, 2022 · Apr 11, 2022 · Apr 11, 2022 · Apr 11, 2022
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -51,7 +51,7 @@ General algebra:
     ring: 'ring'
     ring morphism: 'ring_hom'
     the category of rings: 'Ring'
-    subring: 'is_subring'
+    subring: 'subring'
     localization: 'localization'
     local ring: 'local_ring'
     noetherian ring: 'is_noetherian_ring'

diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -124,7 +124,7 @@ Group Theory:
 Ring Theory:
   Fundamentals:
     ring: 'ring'
-    subrings: 'is_subring'
+    subrings: 'subring'
     ring morphisms: 'ring_hom'
     ring structure $\Z$: 'int.comm_ring'
     product of rings: 'pi.ring'

diff --git a/src/deprecated/group.lean b/src/deprecated/group.lean