bind₂_monomial_one — Mathlib

English

Binding a monomial with unit coefficient acts as the identity on the monomial.

Русский

Связывание монома с единичным коэффициентом действует как тождество на мономе.

LaTeX

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

Lean4

@[simp]
theorem bind₂_monomial_one (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) : bind₂ f (monomial d 1) = monomial d 1 := by
  rw [bind₂_monomial, f.map_one, one_mul]

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