Theorem ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff

Modification history

2025-07-13 19:12
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
chore(Analysis/InnerProductSpace/Adjoint): remove additional hypothesis of completeness when finite (#27068)
Modified ContinuousLinearMap.isSelfAdjoint_toLinearMap_iffView on Github →
2025-06-04 13:46
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat: define `IsPositive` and Löwner order for `LinearMap` (#24471) …
Added ContinuousLinearMap.isSelfAdjoint_toLinearMap_iffView on Github →