mathlib3

806c0bb8 - feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers (#18200)

feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers (#18200) In order for convergence to be well-defined, we put the product topology on `triv_zero_sq_ext R M` via its obvious internal representation as a product. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exponentials.20in.20seminormed.20algebras/near/321870256).