one_smul_eq_id

Mathlib.Algebra.Group.Action.Defs

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

← MathLib Explorer

English

The function mapping x to 1 • x is the identity function on α.

Русский

Функция x ↦ 1 • x равна тождественной на α.

LaTeX

$$$\\\\forall x \\\\in α, \\\\ (1 : M) \\\\cdot x = x.$$$

Lean4

/-- `SMul` version of `one_mul_eq_id` -/
@[to_additive /-- `VAdd` version of `zero_add_eq_id` -/
    ]
theorem one_smul_eq_id : (((1 : M) • ·) : α → α) = id :=
  funext <| one_smul _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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