mulSingle_op — Mathlib

English

For an op with op i 1 = 1 for all i, mulSingle i (op i x) equals the function j ↦ op j (mulSingle i x j).

Русский

Для отображения op с условием op i 1 = 1 для всех i выполняется mulSingle i (op i x) = λ j, op j (mulSingle i x j).

LaTeX

$$$(\forall i, x,\; mulSingle i (op i x) = \lambda j,\; op j (mulSingle i x j))$$$

Lean4

@[to_additive]
theorem mulSingle_op (op : ∀ i, M i → N i) (h : ∀ i, op i 1 = 1) (i : ι) (x : M i) :
    mulSingle i (op i x) = fun j => op j (mulSingle i x j) :=
  .symm <| funext <| apply_mulSingle op h i x

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