English
For an additive group hom f: M →+ M₂, the range under the associated integer-linear map f.toIntLinearMap coincides with AddSubgroup.toIntSubmodule of the range of f.
Русский
Для гомоморфизма абстрактных групп f: M →+ M₂ образ f.toIntLinearMap совпадает с AddSubgroup.toIntSubmodule образа f.
LaTeX
$$$\operatorname{range} f.toIntLinearMap = \operatorname{AddSubgroup}.toIntSubmodule (\operatorname{range} f)$$$
Lean4
/-- Restrict the codomain of a linear map `f` to `f.range`.
This is the bundled version of `Set.rangeFactorization`. -/
abbrev rangeRestrict [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : M →ₛₗ[τ₁₂] LinearMap.range f :=
f.codRestrict (LinearMap.range f) (LinearMap.mem_range_self f)