fix(blueprint): declaration name, for the mathlib bump

leanprover-community · Jan 17, 2025 · 29c536b · 29c536b
1 parent b57f92d
commit 29c536b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/blueprint/src/global_convex_integration.tex b/blueprint/src/global_convex_integration.tex
@@ -330,7 +330,7 @@ \subsection{Jets spaces}
 
 \begin{lemma}
 \label{lem:one_jet_extension_prop}
-\lean{Smooth.oneJetExt}
+\lean{ContMDiff.oneJetExt}
 \leanok
 \uses{def:one_jet_extension}
 For every smooth map $f \co M → N$,