Theorem LinearMap.isSelfAdjoint_iff_map_star

Modification history

2025-10-23 20:09
Mathlib/Algebra/Star/LinearMap.lean
feat(Algebra/Star): define the intrinsic star on linear maps (#29941) …
Added LinearMap.isSelfAdjoint_iff_map_starView on Github →