Results on DualNumber R related to the norm #
These are just restatements of similar statements about TrivSqZeroExt R M.
Main results #
@[simp]
theorem
DualNumber.exp_eps
(𝕜 : Type u_1)
{R : Type u_2}
[Field 𝕜]
[CharZero 𝕜]
[CommRing R]
[Algebra 𝕜 R]
[UniformSpace R]
[TopologicalRing R]
[T2Space R]
:
NormedSpace.exp 𝕜 DualNumber.eps = 1 + DualNumber.eps
@[simp]
theorem
DualNumber.exp_smul_eps
(𝕜 : Type u_1)
{R : Type u_2}
[Field 𝕜]
[CharZero 𝕜]
[CommRing R]
[Algebra 𝕜 R]
[UniformSpace R]
[TopologicalRing R]
[T2Space R]
(r : R)
:
NormedSpace.exp 𝕜 (r • DualNumber.eps) = 1 + r • DualNumber.eps