mathlib3 documentation


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 #

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) :