nontriviality R
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
⊢ homogenization i (X j + C r) = X j + C r * X i
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ homogenization i (X j + C r) = X j + C r * X i