mulSingle_eq_same

Mathlib.Algebra.Notation.Pi.Basic

URI: https://scilib.ai/kg/mathlib#Pi.mulSingle_eq_same

English

Updating the i-th coordinate of a family of types M i by x, and selecting i, yields x.

Русский

Обновление i-й координаты семейства функций, замещая её на x, даёт x в точке i.

LaTeX

$$mulSingle i x i = x$$

Lean4

@[to_additive (attr := simp)]
theorem mulSingle_eq_same (i : ι) (x : M i) : mulSingle i x i = x :=
  Function.update_self i x _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru