English
Variant of the above with a direct product decomposition for disjoint unions without changing the commuting structure.
Русский
Вариант выше с прямым разложением на произведения для дискретных объединений без изменения коммутативности.
LaTeX
$$$ (s,t) \text{ disjoint} \Rightarrow \; (s \cup t).noncommProd f comm = s.noncommProd f (comm.mono ...) \; * \; t.noncommProd f (comm.mono ...) $$$
Lean4
/-- The non-commutative version of `Finset.prod_union` -/
@[to_additive /-- The non-commutative version of `Finset.sum_union` -/
]
theorem noncommProd_union_of_disjoint [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (f : α → β)
(comm : {x | x ∈ s ∪ t}.Pairwise (Commute on f)) :
noncommProd (s ∪ t) f comm =
noncommProd s f (comm.mono <| coe_subset.2 subset_union_left) *
noncommProd t f (comm.mono <| coe_subset.2 subset_union_right) :=
by
obtain ⟨sl, sl', rfl⟩ := exists_list_nodup_eq s
obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t
rw [List.disjoint_toFinset_iff_disjoint] at h
calc
noncommProd (List.toFinset sl ∪ List.toFinset tl) f comm
_ = noncommProd ⟨↑(sl ++ tl), Multiset.coe_nodup.2 (sl'.append tl' h)⟩ f (by convert comm; simp [Set.ext_iff]) :=
(noncommProd_congr (by ext; simp) (by simp) _)
_ =
noncommProd (List.toFinset sl) f (comm.mono <| coe_subset.2 subset_union_left) *
noncommProd (List.toFinset tl) f (comm.mono <| coe_subset.2 subset_union_right) :=
by simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl']
