mulSingle_comm — Mathlib

English

The operation mulSingle is symmetric in its index and the value: (mulSingle i x) j = (mulSingle j x) i.

Русский

Операция mulSingle симметрична по индексам и значению: (mulSingle i x) j = (mulSingle j x) i.

LaTeX

$$$ (mulSingle i x j) = (mulSingle j x i) $$$

Lean4

/-- On non-dependent functions, `Pi.mulSingle` is symmetric in the two indices. -/
@[to_additive /-- On non-dependent functions, `Pi.single` is symmetric in the two indices. -/
    ]
theorem mulSingle_comm (i : ι) (x : M) (j : ι) : (mulSingle i x : ι → M) j = (mulSingle j x : ι → M) i := by
  simp [mulSingle_apply, eq_comm]

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