X_pow_mul_assoc_C — Mathlib

English

A loop-avoiding simplification: constants can be placed to the left of X^n in a product: p · X^n · C(r) = p · C(r) · X^n.

Русский

Упрощение без цикла: константы можно ставить слева от X^n в произведении: p · X^n · C(r) = p · C(r) · X^n.

LaTeX

$$$p \\cdot X^{n} \\cdot C(r) = p \\cdot C(r) \\cdot X^{n}$$$

Lean4

/-- Prefer putting constants to the left of `X ^ n`.

This lemma is the loop-avoiding `simp` version of `X_pow_mul_assoc`. -/
@[simp]
theorem X_pow_mul_assoc_C {n : ℕ} (r : R) : p * X ^ n * C r = p * C r * X ^ n :=
  X_pow_mul_assoc

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