F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ eval x (basisDivisor x y) = 1
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X]
no goals
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1
exact inv_mul_cancel (sub_ne_zero_of_ne hxy)