rw [sub_eq_add_neg, sub_eq_add_neg, ← C_neg, homogenization_X_add_C, C_neg, neg_mul]
R✝ : Type ?u.241614
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
r : R
⊢ homogenization i (X j - C r) = X j - C r * X i
no goals