bind₂_monomial — Mathlib

English

Binding a monomial with coefficient r results in the coefficient applied to the monomial with unit exponents, i.e., f(r) times the monomial with exponent 1 on each index in the support.

Русский

Связывание монома с коэффициентом r приводит к применению коэффициента f(r) к моному с единичными степенями на индексах в опоре.

LaTeX

$$$$ \mathrm{bind}_2\, f\; (\mathrm{monomial}\; d\; r) = f(r) \cdot \mathrm{monomial}\; d\; 1 $$$$

Lean4

theorem bind₂_monomial (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R) :
    bind₂ f (monomial d r) = f r * monomial d 1 := by
  simp only [monomial_eq, RingHom.map_mul, bind₂_C_right, Finsupp.prod, map_prod, map_pow, bind₂_X_right, C_1, one_mul]

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