Commit 2025-09-27 10:18 6576717c

View on Github →

feat(Algebra/Module/LinearMap): range (f.smulRight x) = span {x} (#28350)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/LinearMap/DivisionRing.lean

added theorem LinearMap.range_smulRight_apply

added theorem LinearMap.range_smulRight_apply_of_surjective

added theorem LinearMap.surjective_iff_ne_zero

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

modified theorem Module.Dual.range_eq_top_of_ne_zero

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.range_smulRight_apply