Blueprint: rudin depends on rudin_exp

blueprint/src/chang.tex

@@ -50,7 +50,7 @@ \chapter{Chang's lemma}
 If the discrete Fourier transform of $f : G \longrightarrow \C$ has dissociated support and $p \ge 2$ is an integer, then $\norm{f}_p \le 2 * \sqrt{pe} \norm f_2$.
 \end{lemma}
 \begin{proof}
-\uses{rudin_exp_ineq}
+\uses{rudin_exp}
 \leanok
 It is enough to show that $\norm{\Re f}_p \le \sqrt{pe} \norm f_2$ as then
 $$\norm{f}_p \le \norm{\Re f}_p + \norm{i \Im f}_p = \norm{\Re f}_p + \norm{\Re (-if)}_p \le 2 \sqrt{pe} \norm f_2$$