TrivSqZeroExt R M #
TrivSqZeroExt R M inherits the topology from
R × M.
Note that this is not the topology induced by the seminorm on the dual numbers suggested by
this Math.SE answer, which instead induces
the topology pulled back through the projection map
TrivSqZeroExt.fst : tsze R M → R.
Obviously, that topology is not Hausdorff and using it would result in
exp converging to more than
Main results #
TrivSqZeroExt.topologicalRing: the ring operations are continuous
This is not an instance due to complaints by the
fails_quickly linter. At any rate, we only
really care about the
TopologicalRing instance below.