fintypeRange — Mathlib

English

Restrict the codomain of a linear map to its range; this is the bundled form of a range factorization: a map from M to range f that factors f.

Русский

Ограничение кодомапа до диапазона, дающее факторизацию: образуется отображение из M в range f, равное f.

LaTeX

$$$\text{rangeRestrict}[\text{RingHomSurjective }\tau_{12}]\ (f) : M \to_ {\tau_{12}} \operatorname{LinearMap.range} f$$$

Lean4

/-- The range of a linear map is finite if the domain is finite.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype M₂`. -/
instance fintypeRange [Fintype M] [DecidableEq M₂] [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : Fintype (range f) :=
  Set.fintypeRange f

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