one_zpow — Mathlib

English

The identity matrix raised to any integer power equals the identity: I^{n} = I for all n ∈ ℤ.

Русский

Единичная матрица в любой целой степени сохраняет единичность: I^{n} = I для всех n ∈ ℤ.

LaTeX

$$$$I^{n} = I\\quad \\text{for all } n \\in \\mathbb{Z},$$$$

Lean4

@[simp]
theorem one_zpow : ∀ n : ℤ, (1 : M) ^ n = 1
  | (n : ℕ) => by rw [zpow_natCast, one_pow]
  | -[n+1] => by rw [zpow_negSucc, one_pow, inv_one]

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