natTrailingDegree_mul — Mathlib

English

Assuming NoZeroDivisors in R, if p ≠ 0 and q ≠ 0 then (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree.

Русский

При отсутствии нулей делителей в R, если p ≠ 0 и q ≠ 0, то natTrailingDegree произведения равно сумме natTrailingDegree.

LaTeX

$$$ [NoZeroDivisors R] \; hp : p \neq 0 \; hq : q \neq 0 \; (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree $$$

Lean4

theorem natTrailingDegree_mul [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) :
    (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree :=
  natTrailingDegree_mul' (mul_ne_zero (mt trailingCoeff_eq_zero.mp hp) (mt trailingCoeff_eq_zero.mp hq))

Похожие утверждения