English
There is an induction principle for noncommProd: if p is a property closed under combining adjacent elements with respect to commutativity proofs, holds for 1, and holds for every x in s, then p holds for s.noncommProd.
Русский
Для некоммутативного произведения существует принцип индукции: если свойство p сохраняется при объединении соседних элементов с учётом доказательств коммутативности, верно для единицы, и верно для каждого элемента x в s, то верно для s.noncommProd.
LaTeX
$$$p(1) \\quad \\text{and} \\quad (\\forall a,b, p(a) \\to p(b) \\to p(a\\,\\ast\\, b)) \\;\\Rightarrow\\; p(s.noncommProd comm).$$$
Lean4
@[to_additive]
theorem noncommProd_induction (s : Multiset α) (comm) (p : α → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1)
(base : ∀ x ∈ s, p x) : p (s.noncommProd comm) :=
by
induction s using Quotient.inductionOn with
| _ l
simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢
exact l.prod_induction p hom unit base
