scaleRoots_mul — Mathlib

English

For p, q ∈ R[X] and r ∈ R, r^{deg p + deg q − deg(p q)} · (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

Русский

Для p, q ∈ R[X] и r ∈ R верно: r^{deg p + deg q − deg(p q)} · (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

LaTeX

$$$ r^{\operatorname{natDegree}(p) + \operatorname{natDegree}(q) - \operatorname{natDegree}(p q)} \cdot (p q).\scaleRoots r = p.\scaleRoots r \cdot q.\scaleRoots r $$$

Lean4

@[simp]
theorem scaleRoots_mul (p : R[X]) (r s) : p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s := by ext;
  simp [mul_pow, mul_assoc]

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