Documentation

Mathlib.Analysis.Normed.Algebra.DualNumber

Results on DualNumber R related to the norm #

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

Main results #

source
📐 coverage
@[simp]
theorem DualNumber.exp_eps {R : Type u_1} [CommRing R] [Algebra ℚ R] [UniformSpace R] [IsTopologicalRing R] [T2Space R] :
NormedSpace.exp eps = 1 + eps
source
📐 coverage
@[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