Theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'

Modification history

2026-02-10 22:14

Mathlib/Algebra/Star/LinearMap.lean

refactor: add type synonym for convolutive product of linear maps and intrinsic star (#34945) …

Modified LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'View on Github →

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 LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'View on Github →