Theorem Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff

Modification history

2025-11-26 02:38

Mathlib/Algebra/Star/LinearMap.lean

feat(LinearAlgebra/Matrix/ToLin): `star A.toLin' = (A.map star).toLin'` (intrinsic star) (#31221)

Added Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff View on Github →