one_mul_eq_id

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#one_mul_eq_id

English

Left multiplication by 1 is the identity map: (1) · · = id.

Русский

Левое умножение на 1 даёт тождественное отображение: 1 · x = x.

LaTeX

$$$(1) \cdot x = x$ for all x$$

Lean4

@[to_additive]
theorem one_mul_eq_id : ((1 : M) * ·) = id :=
  funext one_mul

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

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

Разделы

Аффилиация

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