Theorem LinearMap.intrinsicStar_smulRight

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_smulRightView on Github →
2025-12-31 01:04
Mathlib/Algebra/Star/LinearMap.lean
feat(Algebra/Star/LinearMap): `LinearMap.intrinsicStar_{toSpanSingleton, smulRight}` (#33395)
Added LinearMap.intrinsicStar_smulRightView on Github →