diff --git a/src/computational_monads/asymptotics/negligable.lean b/src/computational_monads/asymptotics/negligible.lean
similarity index 100%
rename from src/computational_monads/asymptotics/negligable.lean
rename to src/computational_monads/asymptotics/negligible.lean
diff --git a/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean b/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean
index 1852bff..c5040ef 100644
--- a/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean
+++ b/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean
@@ -21,7 +21,7 @@ and further extend this with various assumptions about run times of computations
 -/
 
 open_locale big_operators ennreal
-open oracle_comp oracle_spec
+open oracle_comp oracle_spec asymptotics
 
 /-- An `algorithmic_homogenous_space` is a homogenous space where operations are all `poly_time`.
 Uses mathlib's definition of an `add_torsor`, which is a bijective group action.
diff --git a/src/crypto_foundations/primitives/asymm_enc.lean b/src/crypto_foundations/primitives/asymm_enc.lean
index 20ebcb7..eba6973 100644
--- a/src/crypto_foundations/primitives/asymm_enc.lean
+++ b/src/crypto_foundations/primitives/asymm_enc.lean
@@ -181,6 +181,6 @@ variables {spec : ℕ → oracle_spec} {M PK SK C : ℕ → Type}
 
 def ind_cpa_secure (enc_scheme : asymm_enc_scheme spec M PK SK C) : Prop :=
 ∀ (adv : Π (sp : ℕ), (enc_scheme sp).ind_cpa_adv),
-  negligible (λ sp, (ind_cpa_exp (adv sp)).advantage)
+  asymptotics.negligible (λ sp, (ind_cpa_exp (adv sp)).advantage)
 
 end asymm_enc_scheme
diff --git a/src/crypto_foundations/primitives/hash_function.lean b/src/crypto_foundations/primitives/hash_function.lean
index 824a63d..90055d3 100644
--- a/src/crypto_foundations/primitives/hash_function.lean
+++ b/src/crypto_foundations/primitives/hash_function.lean
@@ -48,6 +48,6 @@ variables {spec : ℕ → oracle_spec} {K I O : ℕ → Type}
   of winning the `collision_finding_experiment` as the security parameter increases -/
 def collision_resistant (hf : hash_scheme spec K I O) : Prop :=
 ∀ (adv : Π (sp : ℕ), (hf sp).collision_finding_adv),
-negligible (λ sp, (collision_finding_exp (adv sp)).advantage)
+  asymptotics.negligible (λ sp, (collision_finding_exp (adv sp)).advantage)
 
 end hash_scheme
\ No newline at end of file