diff --git a/MIL/C07_Structures/S02_Algebraic_Structures.lean b/MIL/C07_Structures/S02_Algebraic_Structures.lean
index 813d75b..26beb30 100644
--- a/MIL/C07_Structures/S02_Algebraic_Structures.lean
+++ b/MIL/C07_Structures/S02_Algebraic_Structures.lean
@@ -625,7 +625,7 @@ instance of another, using the ``extends`` keyword.
 This is how Mathlib specifies that, for example,
 every commutative ring is a ring.
 You can find more information in :numref:`hierarchies` and in a
-`section on class inference <https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#managing-type-class-inference>`_ in *Theorem Proving in Lean*.
+`section on class inference <https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes/#managing-type-class-inference>`_ in *Theorem Proving in Lean*.
 
 In general, it is a bad idea to specify a value of
 ``*`` for an instance of an algebraic structure that already has