one_apply

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.one_apply

English

The function underlying the identity endomorphism sends each element to itself: (1 : End_R(M)) x = x.

Русский

Функция, лежащая в основе идентичного эндоморфизма, отображает каждый элемент в самого себя: (1 : End_R(M)) x = x.

LaTeX

$$$ (1_{\mathrm{End}_R(M)}) (x) = x $$$

Lean4

@[simp]
theorem one_apply (x : M) : (1 : Module.End R M) x = x :=
  rfl

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

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

Разделы

Аффилиация

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