# The minimal unitization of a Cā-algebra #

This file shows that when `E`

is a Cā-algebra (over a densely normed field `š`

), that the minimal
`Unitization`

is as well. In order to ensure that the norm structure is available, we must first
show that every Cā-algebra is a `RegularNormedAlgebra`

.

In addition, we show that in a `RegularNormedAlgebra`

which is a `StarRing`

for which the
involution is isometric, that multiplication on the right is also an isometry (i.e.,
`Isometry (ContinuousLinearMap.mul š E).flip`

).

A Cā-algebra over a densely normed field is a regular normed algebra.

## Equations

- āÆ = āÆ

This is the key lemma used to establish the instance `Unitization.instCStarRing`

(i.e., proving that the norm on `Unitization š E`

satisfies the Cā-property). We split this one
out so that declaring the `CStarRing`

instance doesn't time out.

The norm on `Unitization š E`

satisfies the Cā-property

## Equations

- āÆ = āÆ