simp
case empty
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
⊢ homogenization i (∏ l ∈ ∅, P l) = ∏ l ∈ ∅, homogenization i (P l)
no goals