insertNth_mul — Mathlib

English

Insertion preserves pointwise multiplication: inserting x and y at the same index i with p and q on the tails yields the product of the two inserted results.

Русский

Вставка сохраняет покоординатное умножение: вставляя x и y в одну и ту же позицию i с p и q на хвостах, получаем произведение полученных функций.

LaTeX

$$$ i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q $$$

Lean4

@[to_additive (attr := simp)]
theorem insertNth_mul [∀ j, Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
    i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q :=
  insertNth_binop (fun _ ↦ (· * ·)) i x y p q

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