insertNth_div_same — Mathlib

English

In a family of groups, the quotient of two inserted values with the same tail equals the single coordinate corresponding to the quotient x/y.

Русский

В семье групп отношение частей вставок с одинаковым хвостом даёт единичную координату x/y.

LaTeX

$$$ i.insertNth (x / y) p q = i.insertNth x p / i.insertNth y q = \Pi.mulSingle i (x / y) $$$

Lean4

@[to_additive (attr := simp)]
theorem insertNth_div_same [∀ j, Group (α j)] (i : Fin (n + 1)) (x y : α i) (p : ∀ j, α (i.succAbove j)) :
    i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y) := by
  simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]

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