prod_mul_eq_prod_mul_of_exists — Mathlib

English

If f is a finitely supported function and g is a function with a product identity under the exists condition, then a product equality holds: prod_mul_eq_prod_mul_of_exists: for a, ha in f.support and h such that g a (f a) • n1 = g a (f a) • n2, we have f.prod g • n1 = f.prod g • n2.

Русский

Если существуют условия, обеспечивающие равенство произведений, то произведение с n1 и n2 совпадают.

LaTeX

$$$\text{prod}_g (f) \cdot n_1 = \text{prod}_g (f) \cdot n_2$ при $a \in f.support$, и $g a (f a) n_1 = g a (f a) n_2$.$$

Lean4

@[to_additive]
theorem prod_mul_eq_prod_mul_of_exists [Zero M] [CommMonoid N] {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N} (a : α)
    (ha : a ∈ f.support) (h : g a (f a) * n₁ = g a (f a) * n₂) : f.prod g * n₁ = f.prod g * n₂ := by
  classical exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

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