$\Lambda_i$. Gröbner basis methods for variable elimination then allow one to determine generators of the polynomial ideal of all clade invariants. Such computations were useful in formulating the general construction of certain linear invariants given below. The existence of these clade invariants forms the basis our proof of species tree topology identifiability in Section \[sec:id\].

\[thm:cladeinv\] Let $\mathcal A\subsetneq \mathcal X$ be a subset of taxa with at least two elements, and $\mathcal C\subseteq \mathcal
  X\smallsetminus\mathcal A$ a non-empty set of taxa not in $\mathcal
  A$. For distinct $a,b\in \mathcal A$, let $\mathcal A'=\mathcal
  A\smallsetminus\{a,b\}$. Then if $\mathcal A$ is a clade on $\sigma$, $$\left( \sum_{\mathcal S\subseteq \mathcal A'} {\mathbb P}_\sigma(\mathcal S_g\cup\{A\}\cup \mathcal C_g)\right )
  - \left ( \sum_{\mathcal S\subseteq \mathcal A'}{\mathbb P}_\sigma(\mathcal S_g\cup\{B\}\cup \mathcal C_g)\right )=0.
\label{eq:cladeinv}$$

We note that this theorem applies to any species tree, including non-binary ones. Moreover, since a non-binary species tree $\sigma$ can be thought of as any of its binary resolutions with length 0 assigned to any introduced edges, the clade probabilities arising from such a $\sigma$ will satisfy the polynomials of the theorem for every binary resolution. Thus in the statement of the theorem the phrase ‘if $\mathcal A$ is a clade 