Theorem LinearMap.intrinsicStar_toSpanSingleton

Modification history

2025-12-31 01:04

Mathlib/Algebra/Star/LinearMap.lean

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

Added LinearMap.intrinsicStar_toSpanSingleton View on Github →