Continuity of the Clifford norm

The reverse Clifford norm on the Lipschitz group is continuous over a Hausdorff topological field. Its scalar value is recovered from reverse x * x through the closed embedding of the field into the finite-dimensional Clifford algebra. The inverse coordinate of the unit-valued norm is continuous by the homomorphism law. This is the local topological input for studying the spinor norm through the Clifford norm.

theorem CliffordAlgebra.continuous_cliffordNorm {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : Continuous ⇑(cliffordNorm Q)

The reverse Clifford norm is continuous on the Lipschitz group.