reverse_mul — Mathlib

English

If the product of the leading coefficients of f and g is nonzero, then reverse(f g) = reverse(f) · reverse(g).

Русский

Если произведение ведущих коэффициентов f и g не равно нулю, то reverse(f g) = reverse(f) · reverse(g).

LaTeX

$$$\text{If } f,g \in R[X] \text{ and } f.leadingCoeff \cdot g.leadingCoeff \neq 0, \ \operatorname{reverse}(f g) = \operatorname{reverse}(f) \operatorname{reverse}(g).$$$

Lean4

theorem reverse_mul {f g : R[X]} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) : reverse (f * g) = reverse f * reverse g :=
  by
  unfold reverse
  rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]

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