Theorem LinearMap.smulRight_id

Modification history

2025-12-09 12:40

Mathlib/LinearAlgebra/Span/Basic.lean

chore: missing API for `toSpanSingleton` (#32477) …

Added LinearMap.smulRight_id View on Github →