Theorem AddEquiv.toLinearEquiv_continuousLinearEquiv

Modification history

2026-08-10 23:43
Mathlib/Topology/Algebra/Module/TransferInstance.lean
feat: generalize transfer instance type class assumptions (#42291) …
Added AddEquiv.toLinearEquiv_continuousLinearEquivView on Github →