noncommProd_cons — Mathlib

English

For s a multiset and a, the noncommProd of a :: s equals a times the noncommProd of s under a suitably restricted commutativity witness.

Русский

Для мультиcета s и элемента a неcкоммутативное произведение от a :: s равно a умножить на неcкоммутативное произведение по s с соответствующим ограниченным доказательством коммутативности.

LaTeX

$$$\\mathrm{noncommProd}(a::_m s) comm = a \\cdot \\mathrm{noncommProd}(s)(comm.mono\\;...)$$$

Lean4

@[to_additive (attr := simp)]
theorem noncommProd_cons (s : Multiset α) (a : α) (comm) :
    noncommProd (a ::ₘ s) comm = a * noncommProd s (comm.mono fun _ => mem_cons_of_mem) :=
  by
  induction s using Quotient.inductionOn
  simp

Похожие утверждения