Fix blueprint: remove span_remove_element reference

This theorem was referenced in the blueprint but doesn't exist in the
Lean game code. Removed the \lean{} reference to fix CI build failure.

Author: ZRTMRH

blueprint/lean_decls

@@ -16,7 +16,6 @@ LinearAlgebraGame.subset_linear_independent
 LinearAlgebraGame.superset_span_full
 LinearAlgebraGame.linear_combination_unique
 LinearAlgebraGame.linear_independent_insert_of_not_in_span
-LinearAlgebraGame.span_remove_element
 LinearAlgebraGame.InnerProductSpace_real_v
 LinearAlgebraGame.InnerProductSpace_v
 LinearAlgebraGame.inner_self_real

blueprint/src/chapters/linearindependence/sheet9.tex

@@ -2,8 +2,7 @@ \section{Span After Removing Elements}
 
 \begin{theorem}
   \label{theorem : span_remove_element}
-  \lean{LinearAlgebraGame.span_remove_element}
-  \leanok
+  % Note: This theorem is not implemented in the Lean game code
   \uses{definition : span, definition : linear_independent}
   If $S$ is a set of vectors and $v \in S$ can be written as a linear combination of other vectors in $S \setminus \{v\}$, then $\text{span}(S) = \text{span}(S \setminus \{v\})$.
 \end{theorem}