Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-07 09:25 08ffbbb9

View on Github →

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.

Estimated changes