expand — Mathlib

English

For any Ring R, Ring S and RingHom f, p ∈ mapRingHom f).range iff ∀ n, p.coeff n ∈ f.range.

Русский

Для колец R, S и гомоморфа f: p принадлежит образу mapRingHom f тогда и только тогда, когда коэффициенты p лежат в образе f.

LaTeX

$$$p \\in (\\mathrm{mapRingHom}\\ f).\\mathrm{range} \\iff \\forall n, p.\\mathrm{coeff}(n) \\in f.\\mathrm{range}$$$

Lean4

/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`. -/
noncomputable def expand : R[X] →ₐ[R] R[X] :=
  { (eval₂RingHom C (X ^ p) : R[X] →+* R[X]) with commutes' := fun _ => eval₂_C _ _ }

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