Basic facts about normed algebras #
This file provides small pieces of generic normed-algebra infrastructure used across Tau Ceti.
@[instance_reducible]
noncomputable def
TauCeti.normedAlgebraRatOfReal
{R : Type u_1}
[SeminormedRing R]
[NormedAlgebra ℝ R]
:
A real normed algebra regarded as a rational normed algebra.