prod_sumElim — Mathlib

English

There is a product formula for sumElim: (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) · f₂.prod (g ∘ Sum.inr).

Русский

Существует формула произведения для sumElim: (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) · f₂.prod (g ∘ Sum.inr).

LaTeX

$$$(f_1.sumElim f_2).prod\; g = f_1.prod(g\circ\mathrm{Sum.inl}) \cdot f_2.prod(g\circ\mathrm{Sum.inr})$$$

Lean4

@[to_additive]
theorem prod_sumElim {ι₁ ι₂ α M : Type*} [Zero α] [CommMonoid M] (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M) :
    (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr) := by
  simp [Finsupp.prod, Finset.prod_disjSum]

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