F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ degree (basisDivisor x y) = 1
rw [basisDivisor, degree_mul, degree_X_sub_C, degree_C, zero_add]
no goals
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0
exact inv_ne_zero (sub_ne_zero_of_ne hxy)