English
Under suitable finiteness assumptions and a compatibility condition on cross-terms, the product of two product-incidence functions factors: f1.prod g1 · f2.prod g2 = (f1 f2).prod (g1 g2).
Русский
При подходящих предположениях о конечности и совместимости кросс-терминов произведение двух функций-образов-из двух произведений распадается: f1.prod g1 · f2.prod g2 = (f1 f2).prod (g1 g2).
LaTeX
$$$ f_1.prod\ g_1 \ *\ f_2.prod\ g_2 = (f_1 \cdot f_2).prod (g_1 \cdot g_2) $$$
Lean4
/-- This is a version of `IncidenceAlgebra.prod_mul_prod` that works over non-commutative rings. -/
theorem prod_mul_prod' [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)]
(h :
∀ a₁ a₂ a₃ b₁ b₂ b₃, f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)) :
f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂) := by ext x y; simp [Icc_prod_def, sum_mul_sum, h, sum_product]
