zpow_sub — Mathlib

English

Let A be a square matrix with det(A) a unit. For all z1,z2 ∈ ℤ, A^(z1 − z2) = A^z1 / A^z2.

Русский

Пусть A — квадратная матрица с детерминантой, являющейся единицей. Тогда для любых z1,z2 ∈ ℤ выполняется A^(z1 − z2) = A^z1 / A^z2.

LaTeX

$$$ \det(A) \text{ is a unit } \Rightarrow \forall z_1,z_2 \in \mathbb{Z},\ A^{z_1 - z_2} = A^{z_1} / A^{z_2} $$$

Lean4

theorem zpow_sub {A : M} (ha : IsUnit A.det) (z1 z2 : ℤ) : A ^ (z1 - z2) = A ^ z1 / A ^ z2 := by
  rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]

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