Results on DualNumber R related to the norm

These are just restatements of similar statements about TrivSqZeroExt R M.

Main results

• exp_eps

@[simp]

theorem DualNumber.exp_eps (𝕜 : Type u_1) {R : Type u_2} [IsROrC 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] [TopologicalRing R] [CompleteSpace R] [T2Space R] : exp 𝕜 DualNumber.eps = 1 + DualNumber.eps

@[simp]

theorem DualNumber.exp_smul_eps (𝕜 : Type u_1) {R : Type u_2} [IsROrC 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] [TopologicalRing R] [CompleteSpace R] [T2Space R] (r : R) : exp 𝕜 (r • DualNumber.eps) = ↑1 + r • DualNumber.eps