English
If f,g are MonoidAlgebra elements with supports that meet UniqueMul at a specific pair a0,b0, then the product coefficient at a0b0 equals f(a0) g(b0).
Русский
Если f и g — элементы MonoidAlgebra с опорой, удовлетворяющей UniqueMul в точке a0,b0, то коэффициент умножения при a0b0 равен f(a0)g(b0).
LaTeX
$$$$ (f*g)(a_0\,b_0) = f(a_0)\; g(b_0) \quad \text{при условии } UniqueMul\ f требованиям. $$$$
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_mul_eq_mul_of_uniqueMul [Mul A] {f g : MonoidAlgebra R A} {a0 b0 : A}
(h : UniqueMul f.support g.support a0 b0) : (f * g) (a0 * b0) = f a0 * g b0 := by
classical
simp_rw [mul_apply, sum, ← Finset.sum_product']
refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]
· refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]
· refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
rcases not_and_or.mp hnotMem with af | bg
· rw [notMem_support_iff.mp af, zero_mul]
· rw [notMem_support_iff.mp bg, mul_zero]
