trailingCoeff_mul — Mathlib

English

For p,q ∈ Polynomial R with NoZeroDivisors, (p q).trailingCoeff = p.trailingCoeff · q.trailingCoeff.

Русский

Для многочленов p,q над R с NoZeroDivisors: (p q).trailingCoeff = p.trailingCoeff · q.trailingCoeff.

LaTeX

$$$\big(p q\big).trailingCoeff = p.trailingCoeff \cdot q.trailingCoeff.$$$

Lean4

theorem trailingCoeff_mul {R : Type*} [Semiring R] [NoZeroDivisors R] (p q : R[X]) :
    (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff := by
  rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff, reverse_leadingCoeff]

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