zpow_zpow_self

Mathlib.LinearAlgebra.Matrix.ZPow

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

English

For any square matrix A and any integers m,n, A^{m} and A^{n} commute: Commute(A^{m}, A^{n}).

Русский

Для любой квадратной матрицы A и любых целых m,n матрицы A^{m} и A^{n} коммутируют.

LaTeX

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

Lean4

theorem zpow_zpow_self (A : M) (m n : ℤ) : Commute (A ^ m) (A ^ n) :=
  Commute.zpow_zpow (Commute.refl A) _ _

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

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

Разделы

Аффилиация

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