English
If a is not in s, the noncommutative product over insert a s equals f(a) times the noncommProd over s with a tail commutation adjusted.
Русский
Если a не принадлежит s, то некоммопрод по insert a s равен f(a) умножить на некоммопрод по s с учётом изменённого хвостового коммутатива.
LaTeX
$$$ [DecidableEq \alpha] \; (s : \mathrm{Finset} \; \alpha) \; (a : \alpha) \; (f : \alpha \to \beta) \; (comm) \; (ha : a \notin s) \\; noncommProd (\mathrm{insert}\ a\ s) f comm = f\ a * noncommProd\ s\ f (comm.mono \; \text{fun } _ => \text{mem_insert_of_mem})$$$
Lean4
@[to_additive (attr := simp)]
theorem noncommProd_insert_of_notMem [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm) (ha : a ∉ s) :
noncommProd (insert a s) f comm = f a * noncommProd s f (comm.mono fun _ => mem_insert_of_mem) := by
simp only [← cons_eq_insert _ _ ha, noncommProd_cons]
