mulSingle_one — Mathlib

English

For any index i, applying mulSingle to the unit at i yields the constant unit function: mulSingle i (1 : M_i) = 1.

Русский

Для любого индекса i применение mulSingle к единице в i даёт единичную константную функцию: mulSingle i (1 : M_i) = 1.

LaTeX

$$$ mulSingle\ i\ (1 : M i) = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem mulSingle_one (i : ι) : mulSingle i (1 : M i) = 1 :=
  Function.update_eq_self _ _

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