exp_nsmul

Mathlib.Analysis.Normed.Algebra.MatrixExponential

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

English

For any natural n, exp(n • A) = (exp A)^n.

Русский

Для любого натурального n справедливо exp(n • A) = (exp A)^n.

LaTeX

$$$\\exp\\_\\mathbb{K}(n \\cdot A) = \\exp\\_\\mathbb{K}(A)^n$$$

Lean4

nonrec theorem exp_nsmul (n : ℕ) (A : Matrix m m 𝔸) : exp 𝕂 (n • A) = exp 𝕂 A ^ n :=
  open scoped Norms.Operator in exp_nsmul n A

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

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

Разделы

Аффилиация

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