English
Let R be a nontrivial ring. The degree function on polynomials over R extends to a monoid homomorphism from the polynomial ring R[X] to the multiplicative monoid of WithBot(ℕ); in particular, deg(pq) corresponds to the product of deg(p) and deg(q) in that multiplicative setting, and deg(1) is the unit.
Русский
Пусть R — надполе без нулевых делителей. Функция степени на многочленах над R естественно образует гомоморфизм моноида из кольца многочленов R[X] в мультипликативный моноид WithBot(ℕ); в частности, deg(pq) соответствует deg(p)·deg(q) в этом множителе, и deg(1) — единица.
LaTeX
$$$\deg: R[X] \to \mathrm{Multiplicative}(\mathrm{WithBot}\;\mathbb{N}) \quad\text{is a monoid hom},\;\; \deg(pq)=\deg(p)\cdot \deg(q), \; \deg(1)=1.$$$
Lean4
/-- `degree` as a monoid homomorphism between `R[X]` and `Multiplicative (WithBot ℕ)`.
This is useful to prove results about multiplication and degree. -/
def degreeMonoidHom [Nontrivial R] : R[X] →* Multiplicative (WithBot ℕ)
where
toFun := degree
map_one' := degree_one
map_mul' _ _ := degree_mul
