product_mul_product_comm — Mathlib

English

The product of products commutes in the expected way: (s1 × t1) * (s2 × t2) = (s1 * s2) × (t1 * t2).

Русский

Произведение произведений ведёт к ожидаемому коммутированию: (s1 × t1) * (s2 × t2) = (s1 * s2) × (t1 * t2).

LaTeX

$$Eq (instHMul.hMul (Finset.instSProd.sprod s1 t1) (Finset.instSProd.sprod s2 t2)) (Finset.instSProd.sprod (instHMul.hMul s1 s2) (instHMul.hMul t1 t2))$$

Lean4

@[to_additive (attr := simp)]
theorem product_mul_product_comm [DecidableEq β] (s₁ s₂ : Finset α) (t₁ t₂ : Finset β) :
    (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂) :=
  mod_cast s₁.toSet.prod_mul_prod_comm s₂ t₁.toSet t₂

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