Theorem LinearMap.range_smulRight_apply_of_surjective

Modification history

2025-09-27 10:18
Mathlib/Algebra/Module/LinearMap/DivisionRing.lean
feat(Algebra/Module/LinearMap): `range (f.smulRight x) = span {x}` (#28350)
Added LinearMap.range_smulRight_apply_of_surjectiveView on Github →