exp_zsmul — Mathlib

English

For z ∈ ℤ and A a matrix, exp(𝕂, z · A) = (exp(𝕂, A))^{z}.

Русский

Для целого z и матрицы A выполняется exp(z A) = exp(A)^{z}.

LaTeX

$$$\exp_{\mathbb{K}}(z \cdot A) = \big(\exp_{\mathbb{K}}(A)\big)^{z}.$$$

Lean4

theorem exp_zsmul (z : ℤ) (A : Matrix m m 𝔸) : exp 𝕂 (z • A) = exp 𝕂 A ^ z :=
  by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · rw [zpow_natCast, natCast_zsmul, exp_nsmul]
  · have : IsUnit (exp 𝕂 A).det := (Matrix.isUnit_iff_isUnit_det _).mp (isUnit_exp _ _)
    rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]

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