case intro.inl
𝕂 : Type u_2
𝔸 : Type u_1
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n

case intro.inr
𝕂 : Type u_2
𝔸 : Type u_1
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)
𝕂 : Type u_2
𝔸 : Type u_1
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
z : ℤ
x : 𝔸
⊢ exp 𝕂 (z • x) = exp 𝕂 x ^ z
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
no goals
case intro.inl
𝕂 : Type u_2
𝔸 : Type u_1
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n
rw [zpow_ofNat, coe_nat_zsmul, exp_nsmul]
no goals
case intro.inr
𝕂 : Type u_2
𝔸 : Type u_1
inst✝³ : IsROrC 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)
rw [zpow_neg, zpow_ofNat, neg_smul, exp_neg, coe_nat_zsmul, exp_nsmul]