erw [homogenization, Finsupp.mapDomain_add]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (X j ^ n) +
      Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (C r) =
    X j ^ n + C r * X i ^ n