English
Let E/F be a field extension and x ∈ E be transcendental over F. Then the family {(x − a)^{-1} : a ∈ F} is linearly independent over F.
Русский
Пусть E/F — расширение полей и x ∈ E является трансцендентальным над F. Тогда множество {(x − a)^{-1} : a ∈ F} линейно независимо над F.
LaTeX
$$$$\text{If } F \le E \text{ are fields and } x \in E \text{ is transcendental over } F, \ \{(x - \alpha)^{-1} : \alpha \in F\} \text{ is }F\text{-linearly independent.}$$$$
Lean4
/-- 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`. -/
theorem linearIndependent_sub_inv {F E : Type*} [Field F] [Field E] [Algebra F E] {x : E} (H : Transcendental F x) :
LinearIndependent F fun a ↦ (x - algebraMap F E a)⁻¹ := by
classical
rw [transcendental_iff] at H
refine linearIndependent_iff'.2 fun s m hm i hi ↦ ?_
have hnz (a : F) : x - algebraMap F E a ≠ 0 := fun h ↦ X_sub_C_ne_zero a <| H (.X - .C a) (by simp [h])
let b := s.prod fun j ↦ x - algebraMap F E j
have h1 : ∀ i ∈ s, m i • (b * (x - algebraMap F E i)⁻¹) = m i • (s.erase i).prod fun j ↦ x - algebraMap F E j :=
fun i hi ↦ by simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]
replace hm := congr(b * $(hm))
simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] at hm
let p : Polynomial F := s.sum fun i ↦ .C (m i) * (s.erase i).prod fun j ↦ .X - .C j
replace hm :=
congr(Polynomial.aeval i
$(H p (by simp_rw [← hm, p, map_sum, map_mul, map_prod, map_sub, aeval_X, aeval_C, Algebra.smul_def])))
have h2 : ∀ j ∈ s.erase i, m j * ((s.erase j).prod fun x ↦ i - x) = 0 := fun j hj ↦
by
have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]
simp_rw [map_zero, p, map_sum, map_mul, map_prod, map_sub, aeval_X, aeval_C, Algebra.algebraMap_self_apply, ←
s.sum_erase_add _ hi, Finset.sum_eq_zero h2, zero_add] at hm
exact
eq_zero_of_ne_zero_of_mul_right_eq_zero
(Finset.prod_ne_zero_iff.2 fun j hj ↦ sub_ne_zero.2 (Finset.ne_of_mem_erase hj).symm) hm
