Commit 2025-11-24 14:11 769bd370

View on Github →

feat: transfer normed spaces and continuous linear equiv's across equ… (#31896) …ivalences Analogous to existing instances for e.g. linear equivalences. This is required for adding Shrink instances for these, which in turns are necessary for making the definition of immersions in #28793 universe-polymorphic.

Estimated changes