rangeRestrict — Mathlib

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)

Похожие утверждения