diff --git a/Mathlib/RingTheory/AdicCompletion/RingHom.lean b/Mathlib/RingTheory/AdicCompletion/RingHom.lean
index 38cbbc8acb6f3c..9815ebe0540077 100644
--- a/Mathlib/RingTheory/AdicCompletion/RingHom.lean
+++ b/Mathlib/RingTheory/AdicCompletion/RingHom.lean
@@ -24,6 +24,8 @@ lifted to a ring homomorphism `R →+* S`.
   of `R` being `I`-adically complete.
 -/
 
+@[expose] public section
+
 open Ideal Quotient
 
 variable {R S : Type*} [NonAssocSemiring R] [CommRing S] (I : Ideal S)