Power basis of L=K(x)

Stream: maths

[Riccardo Brasca]

I have a (finite) field extension $L/K$ and an element $x \in L$ such that $L=K(x)$. What is the best way of considering the power basis of $L$ given by $x$?
Note that docs#intermediate_field.adjoin.power_basis constructs a power basis pb : power_basis K K⟮x⟯. Mathematically $K(x)=L$, but not in Lean (K⟮x⟯ : intermediate_field K L so the equality does not even make sense). Should I define the power basis by hand and loose the API for docs#intermediate_field.adjoin.power_basis or there is a smarter way? (I don't think I need a lot about this power basis so this would be OK.)

[Filippo A. E. Nuccio]

Don't you like docs#power_basis ? Or may be I don't understand your question.

[Riccardo Brasca]

My question is how to define a power basis of $L$ in the situation I described. docs#intermediate_field.adjoin.power_basis morally does it, but not exactly. BTW I just constructed it by hand :)

[Filippo A. E. Nuccio]

Ah, I see.