mathlib3 documentation

analysis.normed_space.dual_number

Results on dual_number R related to the norm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

source
@[simp]
theorem dual_number.exp_eps (𝕜 : Type u_1) {R : Type u_2} [is_R_or_C 𝕜] [normed_comm_ring R] [normed_algebra 𝕜 R] [topological_ring R] [complete_space R] [t2_space R] :
exp 𝕜 dual_number.eps = 1 + dual_number.eps
source
@[simp]
theorem dual_number.exp_smul_eps (𝕜 : Type u_1) {R : Type u_2} [is_R_or_C 𝕜] [normed_comm_ring R] [normed_algebra 𝕜 R] [topological_ring R] [complete_space R] [t2_space R] (r : R) :
exp 𝕜 (r • dual_number.eps) = 1 + r • dual_number.eps