Theorem: MvPolynomial.homogenization_X_pow_sub_C (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R✝ : Type ?u.276957
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
r : R
⊢ homogenization i (X j ^ n - C r) = X j ^ n - C r * X i ^ n
Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← C_neg, homogenization_X_pow_add_C hn, C_neg, neg_mul]
State after:
no goals