English
If the families f and g commute among themselves and across each other on s, then the combined family x ↦ f(x)g(x) also commutes pairwise over s.
Русский
Если пары f и g коммутируют внутри себя и между собой на s, то объединённая пара
x ↦ f(x)g(x) также попарно коммутирует на s.
LaTeX
$$$ (s : \mathrm{Finset} \; \alpha) \; (comm_{ff} : (s : \mathrm{Set} \alpha).{\rm Pairwise} (Commute on f)) (comm_{gg} : (s : \mathrm{Set} \alpha).{\rm Pairwise} (Commute on g)) (comm_{gf} : (s : \mathrm{Set} \alpha).{\rm Pairwise} fun x y => Commute (g x) (f y)) : \\; (s : \mathrm{Set} \alpha).{\rm Pairwise} (fun x y => Commute ((f * g) x) ((f * g) y))$$$
Lean4
@[to_additive]
theorem noncommProd_mul_distrib_aux {s : Finset α} {f : α → β} {g : α → β}
(comm_ff : (s : Set α).Pairwise (Commute on f)) (comm_gg : (s : Set α).Pairwise (Commute on g))
(comm_gf : (s : Set α).Pairwise fun x y => Commute (g x) (f y)) :
(s : Set α).Pairwise fun x y => Commute ((f * g) x) ((f * g) y) :=
by
intro x hx y hy h
apply Commute.mul_left <;> apply Commute.mul_right
· exact comm_ff.of_refl hx hy
· exact (comm_gf hy hx h.symm).symm
· exact comm_gf hx hy h
· exact comm_gg.of_refl hx hy
