add uses

blueprint/src/sections/dpi_div.tex

@@ -106,7 +106,7 @@ \section{Generic divergences}
   \label{lem:div_comp_le_div_compProd_right}
   %\lean{}
   %\leanok
-  \uses{def:div, def:dpi}
+  \uses{def:div, def:condDiv, def:dpi}
   Let $D$ be a divergence that satisfies the DPI and for which $D(\kappa, \eta \mid \mu) = D(\mu \otimes \kappa, \mu \otimes \eta)$.
   Let $\mathcal \mu \in \mathcal M(\mathcal X)$ and let $\kappa, \eta : \mathcal X \rightsquigarrow \mathcal Y$ be Markov kernels. Then
   \begin{align*}