noncommProd_insert_of_notMem' — Mathlib

English

A variant of the insertion rule using cons' that expresses the same multiplication structure with the inserted element moved appropriately.

Русский

Вариант правила вставки через cons', выражающий ту же структуру умножения с перемещением вставленного элемента.

LaTeX

$$$ noncommProd (insert a s) f comm = noncommProd s f (comm.mono ...) * f a $$$

Lean4

@[to_additive]
theorem noncommProd_insert_of_notMem' [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm) (ha : a ∉ s) :
    noncommProd (insert a s) f comm = noncommProd s f (comm.mono fun _ => mem_insert_of_mem) * f a := by
  simp only [← cons_eq_insert _ _ ha, noncommProd_cons']

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