blueprint def of private noncomputable abbrev

Stream: FLT

[Kevin Buzzard]

On branch private-noncomputable-abbrev-F, leanblueprint checkdecls is failing with F is missing. I only need F in this file and currently I pollute the root namespace with it. How should I fix this?

In the LaTeX we have

\begin{definition}
  \lean{F}
  \label{F}
  \leanok
  If $b\in B$ then define the \emph{characteristic polynomial}
  $F_b$ of $b$ to be $\prod_{g\in G}(X-g\cdot b)$.
\end{definition}

and in the Lean we have

private noncomputable abbrev F (b : B) : B[X] := ∏ᶠ τ : G, (X - C (τ • b))

[Edward van de Meent]

could you namespace it and open the namespace in the file? or does that mean the blueprint can't reference it?

[Kevin Buzzard]

Aah thanks, a variant of this has worked. I gave the definition some kind of very long name following the naming convention, linked to that in the blueprint, and then made F an alias of that. Thanks!