English
Same as above, with the explicit equality for the single-index element.
Русский
То же самое, но с явным равенством для элемента с единицей на прочих местах.
LaTeX
$$$ (\\text{noncommPiCoprod } ϕ hcomm) (\\Pi.mulSingle i y) = ϕ_i(y).$$$
Lean4
@[to_additive (attr := simp)]
theorem noncommPiCoprod_mulSingle [DecidableEq ι] (i : ι) (y : N i) :
noncommPiCoprod ϕ hcomm (Pi.mulSingle i y) = ϕ i y :=
by
change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _) = ϕ i y
rw [← Finset.insert_erase (Finset.mem_univ i)]
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ (Finset.notMem_erase i _)]
rw [Pi.mulSingle_eq_same]
rw [Finset.noncommProd_eq_pow_card]
· rw [one_pow]
exact mul_one _
· intro j hj
simp only [Finset.mem_erase] at hj
simp [hj]
