zpow_neg_mul_zpow_self

Mathlib.LinearAlgebra.Matrix.ZPow

URI: https://scilib.ai/kg/mathlib#Matrix.zpow_neg_mul_zpow_self

English

For any integer n and invertible A, A^(-n) A^n = I.

Русский

Для любого целого n и обратимой A выполняется A^(-n) A^n = I.

LaTeX

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

Lean4

theorem zpow_neg_mul_zpow_self (n : ℤ) {A : M} (h : IsUnit A.det) : A ^ (-n) * A ^ n = 1 := by
  rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]

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

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

Разделы

Аффилиация

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