Theorem LinearMap.toMatrix'_intrinsicStar

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.toMatrix'_intrinsicStarView 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.toMatrix'_intrinsicStarView on Github →