isRoot_comp — Mathlib

English

Let p, q ∈ R[X] and r ∈ R. Then r is a root of the composition p ∘ q if and only if p is a root at the value q(r): IsRoot (p ∘ q) r ⇔ IsRoot p (q(r)).

Русский

Пусть p, q ∈ R[X], r ∈ R. Тогда r является корнем композиции p ∘ q тогда и только тогда, когда p имеет корень в значении q(r): IsRoot (p ∘ q) r ⇔ IsRoot p (q(r)).

LaTeX

$$$(p.comp\\ q).IsRoot\\ r \\iff p.IsRoot (q.eval\\ r)$$$

Lean4

theorem isRoot_comp {R} [CommSemiring R] {p q : R[X]} {r : R} : (p.comp q).IsRoot r ↔ p.IsRoot (q.eval r) := by
  simp_rw [IsRoot, eval_comp]

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