Linear independence of transcendental elements

Main result

• Transcendental.linearIndependent_sub_inv: let x : E transcendental over F, then {(x - a)⁻¹ | a : F} is linearly independent over F.

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.