id_pow

Mathlib.Algebra.Module.LinearMap.End

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

English

For every n, the nth power of the identity map is the identity: id^n = id.

Русский

Для любого n степень единичного отображения равна единице: id^n = id.

LaTeX

$$$\\mathrm{id}_M^n = \\mathrm{id}_M$ for all n.$$

Lean4

@[simp]
theorem id_pow (n : ℕ) : (id : End R M) ^ n = .id :=
  one_pow n

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

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

Разделы

Аффилиация

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