English
For multisets s and t, the noncommProd of their sum equals the product of the noncommProds of each part, with appropriate monotone restrictions on the commutativity witness.
Русский
Для мультисетов s и t некоммутативное произведение суммы равно произведению некоммутативных произведений частей, с учётом необходимых ограничений на доказательство коммутативности.
LaTeX
$$$\\mathrm{noncommProd}(s+t) = \\mathrm{noncommProd}\\ s\\, (comm.) \\cdot \\mathrm{noncommProd}\\ t\\ (comm.)$$$
Lean4
@[to_additive]
theorem noncommProd_add (s t : Multiset α) (comm) :
noncommProd (s + t) comm =
noncommProd s (comm.mono <| subset_of_le <| s.le_add_right t) *
noncommProd t (comm.mono <| subset_of_le <| t.le_add_left s) :=
by
rcases s with ⟨⟩
rcases t with ⟨⟩
simp
