English
The trailing degree of a product equals the sum of trailing degrees, under suitable conditions (semiring with no zero divisors).
Русский
Хвостовая степень произведения равна сумме хвостовых степеней, при подходящих условиях.
LaTeX
$$$$ \\operatorname{trailingDegree}(p q) = \\operatorname{trailingDegree}(p) + \\operatorname{trailingDegree}(q). $$$$
Lean4
theorem trailingDegree_mul : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree :=
by
by_cases hp : p = 0
· rw [hp, zero_mul, trailingDegree_zero, top_add]
by_cases hq : q = 0
· rw [hq, mul_zero, trailingDegree_zero, add_top]
· rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
apply WithTop.coe_add
