insertNth_div — Mathlib

English

Insertion respects division: inserting x/y at i with tails p/q yields the quotient of the respective insertions.

Русский

Вставка сохраняет деление: вставляя x/y в i с хвостами p/q получаем частное вставок.

LaTeX

$$$ i.insertNth \left( \frac{x}{y} \right) (p/q) = \frac{i.insertNth x p}{i.insertNth y q} $$$

Lean4

@[to_additive (attr := simp)]
theorem insertNth_div [∀ j, Div (α 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

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