mathlib

08ffbbb9 - feat(analysis/normed_space/operator_norm): normed algebra of continuous linear maps (#3282)

feat(analysis/normed_space/operator_norm): normed algebra of continuous linear maps (#3282) Given a normed space `E`, its continuous linear endomorphisms form a normed ring, and a normed algebra if `E` is nonzero. Moreover, the units of this ring are precisely the continuous linear equivalences.