feat: port Analysis.NormedSpace.DualNumber (#4627)

Mathlib.lean

@@ -568,6 +568,7 @@ import Mathlib.Analysis.NormedSpace.Completion
 import Mathlib.Analysis.NormedSpace.ConformalLinearMap
 import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
 import Mathlib.Analysis.NormedSpace.Dual
+import Mathlib.Analysis.NormedSpace.DualNumber
 import Mathlib.Analysis.NormedSpace.Exponential
 import Mathlib.Analysis.NormedSpace.Extend
 import Mathlib.Analysis.NormedSpace.Extr

Mathlib/Analysis/NormedSpace/DualNumber.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module analysis.normed_space.dual_number
+! leanprover-community/mathlib commit 806c0bb86f6128cfa2f702285727518eb5244390
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.DualNumber
+import Mathlib.Analysis.NormedSpace.TrivSqZeroExt
+
+/-!
+# Results on `DualNumber R` related to the norm
+
+These are just restatements of similar statements about `TrivSqZeroExt R M`.
+
+## Main results
+
+* `exp_eps`
+
+-/
+
+
+namespace DualNumber
+
+open TrivSqZeroExt
+
+variable (𝕜 : Type _) {R : Type _}
+
+variable [IsROrC 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R]
+
+variable [TopologicalRing R] [CompleteSpace R] [T2Space R]
+
+@[simp]
+theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps :=
+  exp_inr _ _
+#align dual_number.exp_eps DualNumber.exp_eps
+
+@[simp]
+theorem exp_smul_eps (r : R) : exp 𝕜 (r • eps : DualNumber R) = 1 + r • eps := by
+  rw [eps, ← inr_smul, exp_inr, Nat.cast_one]
+#align dual_number.exp_smul_eps DualNumber.exp_smul_eps
+
+end DualNumber