mul_comp — Mathlib

English

Let p, q, r be polynomials over a commutative semiring. Then composition with r distributes over multiplication: (p q) ∘ r = (p ∘ r)(q ∘ r).

Русский

Пусть p, q, r — полиномы над коммутативным полукольцом. Тогда композиция с r распределяется по умножению: (p q) ∘ r = (p ∘ r)(q ∘ r).

LaTeX

$$$$(p q).comp r = p.comp r \\cdot q.comp r$$$$

Lean4

@[simp]
theorem mul_comp {R : Type*} [CommSemiring R] (p q r : R[X]) : (p * q).comp r = p.comp r * q.comp r :=
  eval₂_mul _ _

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