mul_sum — Mathlib

English

If 0 is not in the support of f : ℕ →₀ ℕ, then the product over its support of x^(f x) is positive.

Русский

Если 0 не лежит в опоре f : ℕ →₀ ℕ, то произведение по элементам опоры x^(f x) положительно.

LaTeX

$$$0 < \prod_{x \in \operatorname{supp}(f)} x^{f(x)}.$$$

Lean4

theorem mul_sum (b : S) (s : α →₀ R) {f : α → R → S} : b * s.sum f = s.sum fun a c => b * f a c := by
  simp only [Finsupp.sum, Finset.mul_sum]

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