one_apply

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.one_apply

English

For all x, 1 x = x.

Русский

Для всех x выполняется 1 x = x.

LaTeX

$$$\\\\forall x \\\\in \\\\alpha, \\\\ (1 : Perm\\\\alpha) x = x$$$

Lean4

theorem one_apply (x) : (1 : Perm α) x = x :=
  rfl

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

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

Разделы

Аффилиация

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