Commit 2025-06-10 14:32 d6445160

feat(Analysis/InnerProductSpace): exchange range + ker (#25417)

theorem range_le_range_iff_ker_le_ker {U : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hU : U.IsSymmetric) :
    range T ≤ range U ↔ ker U ≤ ker T := by

and the forward direction holds in the infinite dimensional case too. Upstreamed from quantumInfo