monomial_finsupp_sum_index — Mathlib

English

Equality of two monomials is characterized by either identical exponent vectors and coefficients, or both coefficients being zero.

Русский

Равенство двух мономов определяется либо идентичными векторами степеней и коэффициентами, либо оба коэффициента равны нулю.

LaTeX

$$$\mathrm{monomial}(a_1) = \mathrm{monomial}(a_2) \iff (a_1 = a_2) \lor (a_1 = 0 \land a_2 = 0)$$$

Lean4

theorem monomial_finsupp_sum_index {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ) (a : R) :
    monomial (f.sum g) a = C a * f.prod fun a b => monomial (g a b) 1 :=
  monomial_sum_index _ _ _

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