Commit 2026-04-23 17:52 626d4ed4

feat: turn ContinuousLinearMapWOT into a structure (#37905) This was previously an @[irreducible] def, which is a suboptimal design choice for a type synonym to which you want to transport data-carrying instances. Indeed, in the current state it is quite painful to add Ring structure when the domain and codomain coincide, and doing it in the naive (albeit usual) way would immediately lead to diamonds. Therefore, we switch this type synonym to be a one-field structure. In addition, we add Ring and Algebra instances, generalize the existing SMul instances, define composition of these maps, and prove that ContinuousLinearMapWOT forms a semitopological ring (i.e., multiplication is continuous in each variable separately).