Give names to expressions

Stream: new members

[Jakob Scholbach]

Another basic question: inside a proof, how can I give (new) names to objects that have been constructed in the proof. E.g. say, I have constructed some polynomial, but I don't want to repeat / mention its construction every time I use it in the sequel. (E.g., I have some minpoly F x, but I want to say "Let P be the minimal polynomial". If I write have P := minpoly F x, I can't seem to access the fact that it is the minimal polynomial later on(?).

[Adam Topaz]

use let or set instead of have

[Adam Topaz]

e.g. let F := foo or set F := foo with hF

[Adam Topaz]

The difference is that set F := foo with hF will add a proof hF that foo = F, which can be useful sometimes.

[Kevin Buzzard]

have is for proofs, let or, better, set...with is for data.