Automatic real bilinearity from a multiplicative norm (source code)

= Automatic real bilinearity from a multiplicative norm
{title2=$\|xy\|=\|x\|\|y\|$}

Suppose a <ring> has an underlying real <normed vector space> and its norm is multiplicative, without initially assuming real bilinearity of multiplication. For fixed $x$, distributivity makes $y\mapsto xy$ additive, while $\|xy-xz\|=\|x\|\|y-z\|$ makes it continuous. Additivity gives rational scalar compatibility, and continuity extends it to every real scalar. Apply the same argument in the other variable to obtain a <bilinear map>. The norm identity also excludes nonzero <zero divisors>.