coe_pow — Mathlib

English

For every A in SL(n, R) and every m in N, the underlying matrix of A^m equals the m-th power of the underlying matrix: ↑(A^m) = (↑A)^m.

Русский

Для каждого элемента A из SL(n, R) и любого натурального числа m матрица-образ A^m равна m-ой степени базовой матрицы A: ↑(A^m) = (↑A)^m.

LaTeX

$$\forall A \in \mathrm{SL}_n(R), \forall m \in \mathbb{N}, \\uparrow (A^m) = (\uparrow A)^m$$

Lean4

@[simp]
theorem coe_pow (m : ℕ) : ↑ₘ(A ^ m) = ↑ₘA ^ m :=
  rfl

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