Theorem LinearMap.intrinsicStarModule

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) …
Deleted LinearMap.intrinsicStarModuleView on Github →
2025-10-23 20:09
Mathlib/Algebra/Star/LinearMap.lean
feat(Algebra/Star): define the intrinsic star on linear maps (#29941) …
Added LinearMap.intrinsicStarModuleView on Github →