Zulip Chat Archive

Stream: maths

Topic: Power basis of L=K(x)


Riccardo Brasca (Nov 10 2021 at 16:25):

I have a (finite) field extension L/KL/K and an element xLx \in L such that L=K(x)L=K(x). What is the best way of considering the power basis of LL given by xx?
Note that docs#intermediate_field.adjoin.power_basis constructs a power basis pb : power_basis K K⟮x⟯. Mathematically K(x)=LK(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 (Nov 15 2021 at 17:31):

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

Riccardo Brasca (Nov 15 2021 at 17:39):

My question is how to define a power basis of LL 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 (Nov 15 2021 at 17:41):

Ah, I see.


Last updated: Dec 20 2023 at 11:08 UTC