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 {R : Type u_1} [CommRing R] [Algebra ℚ R] [UniformSpace R] [IsTopologicalRing R] [T2Space R] : NormedSpace.exp eps = 1 + eps

@[simp]

theorem DualNumber.exp_smul_eps {R : Type u_1} [CommRing R] [Algebra ℚ R] [UniformSpace R] [IsTopologicalRing R] [T2Space R] (r : R) : NormedSpace.exp (r • eps) = 1 + r • eps