zpow

Mathlib.LinearAlgebra.Matrix.ZPow

URI: https://scilib.ai/kg/mathlib#Matrix.IsSymm.zpow

English

If A is symmetric, then A^k is symmetric for every integer k.

Русский

Если A симметрична, то A^k симметрична для любого целого k.

LaTeX

$$$ A.IsSymm \Rightarrow \forall k \in \mathbb{Z}, (A^k).IsSymm $$$

Lean4

theorem zpow {A : M} (h : A.IsSymm) (k : ℤ) : (A ^ k).IsSymm := by rw [IsSymm, transpose_zpow, h]

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

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

Разделы

Аффилиация

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