F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y
F : Type u_1
inst✝ : Field F
x y : F
hxy : basisDivisor x y = 0
⊢ x = y
simp_rw [basisDivisor, mul_eq_zero, X_sub_C_ne_zero, or_false_iff, C_eq_zero, inv_eq_zero,
  sub_eq_zero] at hxy
no goals
F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y
exact hxy