zpow_mul' — Mathlib

English

Let A be a square matrix with det(A) a unit. Then for all integers m,n, A^(m n) = (A^n)^m.

Русский

Пусть A — квадратная матрица, детерминант которой является единицей. Тогда для любых целых m,n выполняется A^(m n) = (A^n)^m.

LaTeX

$$$ \det(A) \text{ is a unit } \Rightarrow \forall m,n \in \mathbb{Z},\ A^{m n} = (A^n)^m $$$

Lean4

theorem zpow_mul' (A : M) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ n) ^ m := by rw [mul_comm, zpow_mul _ h]

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