noncommProd_cons' — Mathlib

English

A refined version of the previous result, giving an explicit expression for (a :: s).noncommProd comm in terms of noncommProd s … and a, with explicit commutativity conditions.

Русский

Уточнённая версия предыдущего результата, дающая явное выражение (a :: s).noncommProd comm через неcкоммутативное произведение по s и a с явными условиями коммутативности.

LaTeX

$$$ (a::_m s).noncommProd comm = (noncommProd s (comm.mono (fun _ => mem_cons_of_mem))) * a $$$

Lean4

@[to_additive]
theorem noncommProd_cons' (s : Multiset α) (a : α) (comm) :
    noncommProd (a ::ₘ s) comm = noncommProd s (comm.mono fun _ => mem_cons_of_mem) * a :=
  by
  induction s using Quotient.inductionOn with
  | _ s
  simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
  induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

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