Theorem ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap

Modification history

2025-06-04 13:46
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat: define `IsPositive` and Löwner order for `LinearMap` (#24471) …
Added ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMapView on Github →