English
If s1 = s2 and the second function coincides with the first on s2, then the noncommProd with respect to s1 equals the noncommProd with respect to s2 with the corresponding function, provided the commuting condition holds.
Русский
Если s1 = s2 и вторая функция совпадает с первой на s2, то некоммопрод по s1 равен некоммопродукту по s2 с соответствующей функцией при условии коммутативности.
LaTeX
$$$ (s_1 = s_2) \Rightarrow \bigl( \forall x \in s_2, f x = g x\bigr) \Rightarrow noncommProd s_1 f comm = noncommProd s_2 g (comm) $$$
Lean4
@[to_additive (attr := simp)]
theorem noncommProd_cons (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm) :
noncommProd (cons a s ha) f comm = f a * noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr) := by
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]
