scaleRoots_eval₂_mul — Mathlib

English

If p divides q, then p.scaleRoots r divides q.scaleRoots r for a unit r, otherwise in general setting.

Русский

Если p делит q, то p.scaleRoots r делит q.scaleRoots r при единице r; в общем виде аналогично.

LaTeX

$$$p \mid q \Rightarrow p.scaleRoots(r) \mid q.scaleRoots(r)$$$

Lean4

theorem scaleRoots_eval₂_mul {p : S[X]} (f : S →+* R) (r : R) (s : S) :
    eval₂ f (f s * r) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f r p :=
  scaleRoots_eval₂_mul_of_commute f r s (mul_comm _ _) fun _ _ ↦ mul_comm _ _

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