monomial_eq_monomial_iff — Mathlib

English

A second variant asserting that the sum over monomials under a linear map equals the evaluation at the sum.

Русский

Второй вариант утверждает, что сумма по мономам под линейным отображением равна значению в сумме.

LaTeX

$$$\sum (\mathrm{monomial}(u,r)) \; b = b(u,r)$$$

Lean4

theorem monomial_eq_monomial_iff {α : Type*} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R) :
    monomial a₁ b₁ = monomial a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 :=
  Finsupp.single_eq_single_iff _ _ _ _

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