range_toAddSubgroup — Mathlib

English

The range of a linear map is finite when the domain is finite (provided surjectivity of τ₁₂).

Русский

Диапазон линейного отображения конечен, если область определения конечно многомерна (при условии сюръективности τ₁₂).

LaTeX

$$$\text{Fintype } M \Rightarrow \operatorname{Fintype}(\operatorname{range} f)$$$

Lean4

theorem range_toAddSubgroup [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
    (range f).toAddSubgroup = f.toAddMonoidHom.range :=
  rfl

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