Lean-Workbook Plus 54222: Degree of a polynomial product

For polynomials $f,g$ with integer coefficients, $\deg(fg)=\deg f+\deg g$. The zero polynomial has extended degree $-\infty$, represented by Lean's bottom value.

Source: Lean-Workbook row lean_workbook_plus_54222 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.