coe_range — Mathlib

English

The set-theoretic range of a linear map f coincides with the range as a submodule when viewed as a set.

Русский

Образ линейного отображения совпадает с диапазоном как подмодуль, если смотреть как множество.

LaTeX

$$$ (\operatorname{range} f : Set M_2) = \operatorname{Set.range} (f)$$$

Lean4

theorem coe_range [RingHomSurjective τ₁₂] (f : F) : (range f : Set M₂) = Set.range f :=
  rfl

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