English
A variant of the cons-based expansion that mirrors the previous cons rule but with the swapped factor order.
Русский
Вариант expansion через cons′, отражающий ту же структуру с изменённым порядком множителей.
LaTeX
$$$ noncommProd (cons a s ha) f comm = noncommProd s f (comm.mono (\; fun _ => Finset.mem_cons.2 ∘ .inr)) * f a $$$
Lean4
/-- The non-commutative version of `Finset.prod_mul_distrib` -/
@[to_additive /-- The non-commutative version of `Finset.sum_add_distrib` -/
]
theorem noncommProd_mul_distrib {s : Finset α} (f : α → β) (g : α → β) (comm_ff comm_gg comm_gf) :
noncommProd s (f * g) (noncommProd_mul_distrib_aux comm_ff comm_gg comm_gf) =
noncommProd s f comm_ff * noncommProd s g comm_gg :=
by
induction s using Finset.cons_induction_on with
| empty => simp
| cons x s hnotMem
ih =>
rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
(comm_gf.mono fun _ => mem_cons_of_mem),
(noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm
