Theorem ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff

Modification history

2026-02-18 12:06
Mathlib/Topology/Algebra/Star/LinearMap.lean
feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps (#33397)
Added ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iffView on Github →