Linear independence of transcendental elements #
Main result #
Transcendental.linearIndependent_sub_inv: letx : Etranscendental overF, then{(x - a)⁻¹ | a : F}is linearly independent overF.
theorem
Transcendental.linearIndependent_sub_inv
{F : Type u_1}
{E : Type u_2}
[Field F]
[Field E]
[Algebra F E]
{x : E}
(H : Transcendental F x)
:
LinearIndependent F fun (a : F) => (x - (algebraMap F E) a)⁻¹
If E / F is a field extension, x is an element of E transcendental over F,
then {(x - a)⁻¹ | a : F} is linearly independent over F.