simp [hq]
case pos
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : q = 0
⊢ homogenization i (p * q) = homogenization i p * homogenization i q
no goals