Commit 2025-12-31 01:04 c8a8a812

View on Github →

feat(Algebra/Star/LinearMap): LinearMap.intrinsicStar_{toSpanSingleton, smulRight} (#33395)

Estimated changes

Modified Mathlib/Algebra/Star/LinearMap.lean

added theorem LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr

added theorem LinearMap.intrinsicStar_eq_comp

added theorem LinearMap.intrinsicStar_smulRight

added theorem LinearMap.intrinsicStar_toSpanSingleton