--- a/src/HOL/Number_Theory/Number_Theory.thy Tue Apr 15 15:17:25 2025 +0200 +++ b/src/HOL/Number_Theory/Number_Theory.thy Tue Apr 15 17:38:20 2025 +0200 @@ -11,6 +11,7 @@ Pocklington Prime_Powers Residue_Primitive_Roots + Modular_Inverse begin end