bind₁_monomial — Mathlib

English

The action of bind₁ on a monomial is the product of the images of each variable raised to its exponent, scaled by the constant coefficient.

Русский

Действие bind₁ на моном содержит произведение образов переменных, возведённых в соответствующие степени, умноженное на константу C(р).

LaTeX

$$$$ \mathrm{bind}_1\, f\, (\mathrm{monomial}\; d\; r) = \mathbf{C}(r) \cdot \prod i \in d.\mathrm{support}, f(i)^{d(i)} $$$$

Lean4

theorem bind₁_monomial (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R) :
    bind₁ f (monomial d r) = C r * ∏ i ∈ d.support, f i ^ d i := by
  simp only [monomial_eq, map_mul, bind₁_C_right, Finsupp.prod, map_prod, map_pow, bind₁_X_right]

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