Theorem Equiv.toLinearEquiv_continuousLinearEquiv

Modification history

2026-08-10 23:43
Mathlib/Topology/Algebra/Module/TransferInstance.lean
feat: generalize transfer instance type class assumptions (#42291) …
Deleted Equiv.toLinearEquiv_continuousLinearEquivView on Github →
2025-11-24 14:11
Mathlib/Topology/Algebra/Module/TransferInstance.lean
feat: transfer normed spaces and continuous linear equiv's across equ… (#31896) …
Added Equiv.toLinearEquiv_continuousLinearEquivView on Github →