MultilinearMap.domCoprod_domDomCongr_sumCongr

theorem MultilinearMap.domCoprod_domDomCongr_sumCongr : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {ι₃ : Type u_4} {ι₄ : Type u_5} [inst : CommSemiring R] {N₁ : Type u_6} [inst_1 : AddCommMonoid N₁] [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : Type u_8} [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (σa : ι₁ ≃ ι₃) (σb : ι₂ ≃ ι₄), MultilinearMap.domDomCongr (σa.sumCongr σb) (a.domCoprod b) = (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)

The theorem `MultilinearMap.domCoprod_domDomCongr_sumCongr` states that for any commutative semiring `R`, additive commutative monoids `N₁`, `N₂`, and `N`, and modules `N₁`, `N₂`, and `N` over `R`, given two multilinear maps `a` and `b` from `N` to `N₁` and `N₂` respectively, and equivalent types `σa : ι₁ ≃ ι₃` and `σb : ι₂ ≃ ι₄`, the domain-domain congruence of the sum of `σa` and `σb` applied to the domain coproduct of `a` and `b` equals the domain coproduct of the domain-domain congruences of `a` and `b` with `σa` and `σb` respectively. This theorem establishes a distributive property of the `domDomCongr` function over the `domCoprod` function in the context of multilinear maps and type equivalences.

More concisely: For any commutative semiring R, additive commutative monoids N₁, N₂, and N, and modules N₁, N₂, and N over R, given multilinear maps a : N -> N₁ and b : N -> N₂, and type equivalences σa : ι₁ ≃ ι₃ and σb : ι₂ ≃ ι₄, the domain-domain congruences of a and b under σa and σb respectively are distributive over the domain coproduct of a and b.