English
The noncommutative product over a cons a s equals the product of f(a) with the noncommProd over s with a reduced commutation in the tail.
Русский
Некоммопрод по последовательности cons a s равно произведению f(a) на некоммопрод по умолчанию для остатка s с ослабленным условием коммутативности.
LaTeX
$$$ \text{noncommProd} (\mathrm{cons}\ a\ s\ ha)\ f\ comm = \mathrm{noncommProd} s\ f (comm.mono ...) \cdot f(a) $$$
Lean4
@[to_additive]
theorem noncommProd_cons' (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm) :
noncommProd (cons a s ha) f comm = noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr) * f a := by
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']
