Theorem LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr

Modification history

2025-12-31 01:04

Mathlib/Algebra/Star/LinearMap.lean

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

Added LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr View on Github →