𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff 𝕜 (↑n) exp
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ∀ {n : ℕ∞}, ContDiff 𝕜 n exp
refine' @(contDiff_all_iff_nat.2 fun n => ?_)
no goals
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
this : ContDiff ℂ (↑n) exp
⊢ ContDiff 𝕜 (↑n) exp
exact this.restrict_scalars 𝕜
case zero
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ContDiff ℂ (↑Nat.zero) exp

case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑(Nat.succ n)) exp
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff ℂ (↑n) exp
induction' n with n ihn
no goals
case zero
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ContDiff ℂ (↑Nat.zero) exp
exact contDiff_zero.2 continuous_exp
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ Differentiable ℂ exp ∧ ContDiff ℂ (↑n) (deriv exp)
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑(Nat.succ n)) exp
rw [contDiff_succ_iff_deriv]
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑n) (deriv exp)
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ Differentiable ℂ exp ∧ ContDiff ℂ (↑n) (deriv exp)
use differentiable_exp
no goals
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑n) (deriv exp)
rwa [deriv_exp]