mul_apply_add_eq_mul_of_uniqueAdd

English

The coefficient of a monomial in a product f*g that can be reached in at most one way as a product of monomials in the supports of f and g is a product.

Русский

Коэффициент монома в произведении f*g, достигаемый как произведение мономов в опорных множествах f и g единственным образом, равен их произведению.

LaTeX

$$$f*g(a_0+b_0) = f(a_0) \cdot g(b_0)$ под условием UniqueAdd$f.support,g.support,a_0,b_0$$$

Lean4

/-- The coefficient of a monomial in a product `f * g` that can be reached in at most one way
as a product of monomials in the supports of `f` and `g` is a product. -/
theorem mul_apply_add_eq_mul_of_uniqueAdd [Add A] {f g : R[A]} {a0 b0 : A} (h : UniqueAdd f.support g.support a0 b0) :
    (f * g) (a0 + b0) = f a0 * g b0 :=
  MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h

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