zpow_self

Mathlib.LinearAlgebra.Matrix.ZPow

URI: https://scilib.ai/kg/mathlib#Matrix.Commute.zpow_self

English

For any square matrix A and any integer n, A^{n} commutes with A itself: Commute(A^{n}, A).

Русский

Для любой квадратной матрицы A и любого целого n выполняется Commute(A^{n}, A).

LaTeX

$$$$\\text{Commute}(A^{n}, A) \\quad (n\\in\\mathbb{Z}).$$$$

Lean4

theorem zpow_self (A : M) (n : ℤ) : Commute (A ^ n) A :=
  Commute.zpow_left (Commute.refl A) _

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

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

Разделы

Аффилиация

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