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]