Commit 2025-11-26 02:38 6647d123

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Star/LinearMap.lean

added theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star

added theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'

deleted theorem LinearMap.isSelfAdjoint_iff_map_star

added theorem LinearMap.toMatrix'_intrinsicStar

added theorem Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff

added theorem Matrix.intrinsicStar_toLin'