Theorems · Theorem · field theory

Transcendental.linearIndependent_sub_inv

∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  Transcendental F x → LinearIndependent F fun a => (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.

Defined in

Mathlib.RingTheory.Algebraic.LinearIndependent

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra