Theorem Matrix.intrinsicStar_toLin'

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 Matrix.intrinsicStar_toLin'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 Matrix.intrinsicStar_toLin'View on Github →