noncommPiCoprod_mulSingle — Mathlib

English

In the commuting family situation, if i is fixed and y ∈ H_i, then the canonical coproduct map sends the element with y in the i-th slot and identity elsewhere to y in G.

Русский

В случае коммутируемого семейства при фиксированном индексе i и элементе y ∈ H_i канонический копродуктовый гомоморфизм отправляет элемент с y в i-ом слоте и единицами в остальных слотах в элемент y в G.

LaTeX

$$$\big(\text{noncommPiCoprod } hcomm\big)(\Pi\text{mulSingle}_i y) = y$$$

Lean4

@[to_additive (attr := simp)]
theorem noncommPiCoprod_mulSingle [DecidableEq ι]
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} (i : ι) (y : H i) :
    noncommPiCoprod hcomm (Pi.mulSingle i y) = y := by apply MonoidHom.noncommPiCoprod_mulSingle

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