contract — Mathlib

English

The opposite of expansion: contraction sends ∑ a_n X^{n p} to ∑ a_n X^n.

Русский

Противоположность расширения: контрактирование отправляет ∑ a_n X^{n p} в ∑ a_n X^n.

LaTeX

$$$\operatorname{contract}(p,f) = \sum_{n=0}^{\operatorname{natDegree}(f)} \operatorname{monomial}(n, f.coeff(n\,p))$$$

Lean4

/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/
noncomputable def contract (p : ℕ) (f : R[X]) : R[X] :=
  ∑ n ∈ range (f.natDegree + 1), monomial n (f.coeff (n * p))

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